ITP 2024

Stream: general

[Patrick Massot]

I think I didn’t see a message about it, so let me point out that the list of ITP2024 papers is now public at https://www.viam.science.tsu.ge/itp2024/program. A quick look at the title suggests the following papers involve Lean:

• Dagur Asgeirsson, Towards solid abelian groups: A formal proof of Nöbeling's theorem
• Henning Basold, Peter Bruin and Dominique Lawson, The Directed Van Kampen Theorem in Lean
• Siddharth Bhat, Alex Keizer, Chris Hughes, Andres Goens and Tobias Grosser, Verifying Peephole Rewriting In SSA Compiler IRs
• Joshua Clune, Yicheng Qian, Alexander Bentkamp and Jeremy Avigad, Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory
• Sam Ezeh, Graphical rewriting for diagrammatic reasoning in monoidal categories in Lean4 (Short paper)
• Patrick Massot, Teaching mathematics using Lean and controlled natural language
• Kai Obendrauf, Anne Baanen, Patrick Koopmann and Vera Stebletsova, * Lean Formalization of a Completeness Proof for Coalition Logic with Common Knowledge*
• Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro and Marijn Heule, Formal Verification of the Empty Hexagon Number
• Floris van Doorn and Heather Macbeth, Integrals within integrals: a formalization of the Gagliardo-Nirenberg-Sobolev inequality

[Patrick Massot]

Authors: today is the last day to submit the final version to production (and the submission website is far from perfect so don’t wait until the last minute).

[Patrick Massot]

I just got an update about the submission server. They are running TeXLive 2023 and the listings package from TeXLive 2022 is not compatible. This crashes TeX and the website shows no explanation, only a timeout message. So if you encounter issues, make sure to run TeXLive 2023 (for me it means I should upgrade Ubuntu from 22.04 to 24.04 which is the next LTS).

[Patrick Massot]

This TeX compilation on the cloud things is really tricky. Note that arxiv also switch to TeXLive 2023, so at least we’ve got some consistency.

[Patrick Massot]

I think this issue is worth pinging random members of the author teams @Dagur Asgeirsson, @Siddharth Bhat, @Josh Clune, @Sam Ezeh, @Anne Baanen, @Wojciech Nawrocki, @Floris van Doorn

[Anne Baanen]

Ah, that explains some issues we encountered. Dagstuhl accepts minted so we switched to using that for syntax highlighting.

[Michael Rothgang]

https://github.com/leanprover-community/leanprover-community.github.io/pull/537 adds these papers to the webpage. If you find further conference's papers missing, please speak up!

[Patrick Massot]

This is nice but why did you move the comment explaining how to normalize this file?

[Michael Rothgang]

Bibtool did so, and I didn't notice until now. https://github.com/leanprover-community/leanprover-community.github.io/pull/538 restores the comment.

[Dagur Asgeirsson]

The entries are also missing the tags formalization, about-lean, or about-mathlib that make them appear on https://leanprover-community.github.io/papers.html.

[Dagur Asgeirsson]

We might need some new categories for that page, I don't know which of the three most applies to Patrick's paper about teaching with Lean, for example. I guess most of the papers are in the "Formalization papers using Lean" category though, i.e. the formalization tag.

[Michael Rothgang]

https://github.com/leanprover-community/leanprover-community.github.io/pull/546 adds the missing tags. I categorised all papers as "formalization" --- but am equally happy to change the tag for the duper paper (to match aesop). Or to change aesop to match duper.

[Michael Rothgang]

https://github.com/leanprover-community/leanprover-community.github.io/pull/547 also adds two missing papers from ITP 23. @Martin Dvořák .