Activities

These are some of our current and recent projects:

• Tomáš Skřivan is developing the use of Lean as a scientific programming language. With Feras Saad, Wonyeol Lee, and Jesse Michel he is working on applications of autodifferentiation and probabilistic programming.
• Wojciech Narwrocki is working on a framework for using the internal language of a topos In Lean.
• Joshua Clune is working on a sledgehammer for Lean based on Duper, a proof-producing superposition theorem prover for Lean he developed with Alexander Bentkamp and Yicheng Qian, and LeanAuto, a tool developed by Qian. He is currently working on a relevance filter and, with Haniel Barbosa, he is working on reconstruction of proofs from cvc5.
• Hannah Fechtner is working on formalizing Artin braid groups.
• Cayden Codel, James Gallicchio, and Wojciech Nawrocki are working on a library for interactions between Lean and SAT solvers, verified encodings, and checkers for SAT-based proofs.
• James Gallicchio is working on using Lean to help verify Rust programs in Verus.
• Chase Norman is working on automated reasoning for dependent type theory. 
• Jeremy Avigad and Patrick Massot are still working on Mathematics in Lean.