Recordings

Stream: Big Proof 2025

[Thomas Browning]

Will recordings be available somewhere?

[Junyan Xu]

https://www.youtube.com/@iniseminarroom1

[Thomas Browning]

Thanks!

[Philippe Duchon]

I suppose the videos will be uploaded after the event - right now I didn't manage to find those from yesterday.

[Rémy Degenne]

On the youtube page linked above, go to the "Live" tab

[Rémy Degenne]

You will see the live session (if there is one) but also all the past recordings

[Philippe Duchon]

Thanks! (I did not know the "Live" tab could be for anything not live!)

[Kim Morrison]

I'm failing to find the recordings. Could someone help me e.g. with a link to Emily's talk?

[Anh Nguyễn]

https://www.youtube.com/live/MmQSgjBURuo?si=UITwyY6QwfuwwkcW

[Ching-Tsun Chou]

It appears that the live streamed videos have not been edited, but they can be found under the "Live" tab:
https://www.youtube.com/@iniseminarroom1/streams

[Oliver Butterley]

EDIT: live videos listed below are no longer available, see instead the YT playlist.

Monday:

Kevin Buzzard (Imperial College London)
Formalizing Fermat: how it's going

Emily Riehl (Johns Hopkins University)
Formalizing invisible mathematics: case studies from higher category theory

Mateja Jamnik (University of Cambridge; Cambridge Computer Laboratory)
AI for Math: The Future of Collaborative Discovery

Thomas Hubert (Google DeepMind Technologies Limited)
AlphaProof When RL meets Formal Maths

Tuesday:

Terence Tao (University of California, Los Angeles)
The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale

Floris van Doorn (Universität Bonn)
The Carleson Project: Formalization and Collaboration

Mario Carneiro (Chalmers University of Technology)
Lean Meta-theory: The Proofs behind the Proofs

Alex Kontorovich (Rutgers, The State University of New Jersey)
Rough Structure and Classification, Revisited

María Inés De Frutos Fernández (University of Bonn)
Formalizing the divided power envelope in Lean

Wednesday:

Paola Iannone (University of Edinburgh)
Lean for teaching university mathematics: current work and future research

Fenner Tanswell (Technische Universität Berlin)
Can Mathematics Be Hacked? Infrastructure, Artificial Intelligence, and the Cybersecurity of Mathematical Knowledge

Olivier Bousquet (Google DeepMind Technologies Limited)
Informal to formal and back with LLMs

Thursday:

Angeliki Koutsoukou-Argyraki (Royal Holloway, University of London; University of Cambridge)
A formalisation of a special case of the Union-Closed Conjecture and formal proofs as datasets in the era of LLMs

Albert Jiang
The realist's guide to AI for formal maths research

Manuel Eberl (Universität Innsbruck)
Case Study: Verifying an Efficient Algorithm to Compute Bernoulli Numbers

Alex Best (Harmonic)
Why Reinforcement Learning needs Formal Methods, and Formal Methods need Reinforcement Learning

Bhavik Mehta (Imperial College London)
Formalising Modern Combinatorics

Friday:

William Timothy Gowers (University of Cambridge; Collège de France)
What role is there, if any, for human-oriented automatic theorem proving today?

Wenda Li (University of Edinburgh; University of Cambridge)
Will mathematical theorem proving be solved by scaling laws?

Sophie Morel ENS - Lyon
Lean projects for introverts

Maryna Viazovska (EPFL - Ecole Polytechnique Fédérale de Lausanne)
Formalizing the sphere packing problem in dimension 8

[Peiran Wu]

No live stream for the discussion session? :(

[Ching-Tsun Chou]

I can't find Bhavik Mehta's talk in the YT playlist:

https://youtube.com/playlist?list=PL9-ncTy2ag0GNawev0_soFy_zbFKj8KN5&si=2BIpxB04yWuM9rx0

The link given above also doesn't work.

[Junyan Xu]

It's finally back online:
https://www.youtube.com/watch?v=WMzP-nmrd6g
The YT playlist was out 2 weeks ago, but this video was added 2 days ago.