Seminar Series Details

The Lean Theorem Prover is an interactive proof assistant, which is a software tool for formally writing and verifying mathematical proofs. Machine learning and Lean have been used together to automatically generate mathematical proofs in a process known as neural theorem proving or autoformalization. The theme of the Spring 2023 seminar is a research effort on formalizations of proofs of the Pythagorean theorem, which has implications for studying the topology of the space of proofs of the theorem and for data augmentation for autoformalization. Seminar participants, which may be mathematicians or computer scientists of all academic levels, are expected to contribute to this ongoing project, such as by choosing a proof to formalize. Participants should also have Lean 3 installed on their computer (for installation, please visit https://leanprover-community.github.io/get_started.html). The seminar will include talks by seminar participants on these topics, workshops led by Alex Kontorovich for overcoming difficulties in partial-formalizations, and relevant guest speakers.