A formalisation of a special case of the Union-Closed Conjecture and formal proofs as datasets in the era of LLMs

Add to your list(s) Download to your calendar using vCal

• Angeliki Koutsoukou-Argyraki (Royal Holloway, University of London)
• Thursday 12 June 2025, 09:15-10:15
• Seminar Room 1, Newton Institute.

If you have a question about this talk, please contact nobody.

BPRW03 - Big proof: formalizing mathematics at scale

I will discuss a formalisation in Isabelle/HOL of a proof of a special case of the Union-Closed Conjecture by J. Aaronson, D. Ellis and I. Leader showing that the Union-Closed Conjecture holds for the union-closed family generated by the cyclic translates of any fixed set (joint work with L. C. Paulson). I will then use our formalisation as an example to motivate a discussion raising the question of exploring what design choices to make while developing formal proofs when viewing them as potentially useful datasets for LLMs.

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 1, Newton Institute
• bld31
• dh539

Note that ex-directory lists are not shown.