University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > A formalisation of a special case of the Union-Closed Conjecture and formal proofs as datasets in the era of LLMs

Log in

University Account

External (via Google)

Information on

Subscribing to talks details

Finding a talk details

Adding a talk details

Disseminating talks details

Help and Documentation details

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

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:

Note that ex-directory lists are not shown.

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

📅 Download to calendar (vCal)

⚠️ Important: BPRW03 - Big proof: formalizing mathematics at scale

👤 Speaker: Angeliki Koutsoukou-Argyraki (Royal Holloway, University of London)
📅 Date & Time: Thursday 12 June 2025, 09:15 - 10:15
📍 Venue: Seminar Room 1, Newton Institute

Questions? Contact the organiser

Abstract

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

Included in Lists

Note: Ex-directory lists are not shown.

Log in

🔐 Log In

Information on

ℹ️ Information

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

This talk is included in these lists:

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

Abstract

Included in Lists

Log in

🔐 Log In

Information on

ℹ️ Information

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

This talk is included in these lists:

Other lists

Other talks

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

Abstract

Included in Lists