Zulip Chat Archive

Stream: general

Topic: Is There List of Publications Verified by Proof Assista...

Justin Desrochers (Oct 03 2023 at 20:37):

I was wondering if anyone knows of a list of papers which have accompanying code in some proof assistant language (Lean or otherwise)? I am currently applying for PhD programs and am interested in integrating proof assistants into my future work. I'd like to find some potential supervisors with some proof assistant experience. To be clear, I'm not looking really for a list of Lean developers or papers about Lean, type theory, or construction. Instead I'm looking for examples of people using proof assistants for math research such as in representation theory or algebra.

Ideally we'd have an "verified by proof assistant" arXiv subject that could be added to any paper, but I don't think this currently exists.

Thanks for your help!

Notification Bot (Oct 03 2023 at 20:38):

Justin Desrochers has marked this topic as resolved.

Notification Bot (Oct 03 2023 at 20:38):

Justin Desrochers has marked this topic as unresolved.

Yaël Dillies (Oct 03 2023 at 20:38):

Look at the last section on this page.

Yaël Dillies (Oct 03 2023 at 20:40):

Most papers here are formalisation papers, taking a standard result from the mathematical literature and formalising it, but some are papers which both introduce and formalise a result, or formalise the result of a companion paper.

Kevin Buzzard (Oct 03 2023 at 21:55):

Justin, what you're looking for is vanishingly rare. People are not doing research and using Lean at the same time. People like Yael are taking modern pieces of mathematical research and formalising them in "real time" but my impression is that this is not what you're looking for.

Adam Topaz (Oct 03 2023 at 22:12):

It is rare indeed, but it does exist. Here is one of my examples: https://raw.githubusercontent.com/adamtopaz/CoeffAltPairs/main/main.pdf (using lean3, sorry :sad: )

Adam Topaz (Oct 03 2023 at 22:14):

Although this does fit more in the category of “formalizing research in real time” as opposed to “doing research with lean”

Joachim Breitner (Oct 04 2023 at 08:28):

For non-Lean references, https://www.isa-afp.org/ contains a fair number of mechanized proof of various mathematical results.

Last updated: Dec 20 2023 at 11:08 UTC