Carnegie Mellon University
Dietrich College of Humanities and Social Sciences  ›  Hoskinson Center for Formal Mathematics  ›  Activities

Activities

These are some of our current and recent projects:

  • Mario Carneiro and Scott Morrison have been leading the port of Mathlib to Lean 4. 
  • Tomáš Skřivan is developing the use of Lean as a scientific programming language.
  • Joshua Clune is working with Alexander Bentkamp and Yicheng Qian on Duper, a proof-producing superposition theorem prover for Lean. Qian is visiting Carnegie Mellon in the summer of 2023.
  • Cayden Codel is working on a library of verified encodings for SAT solvers.
  • Codel, Clune, Marijn Heule, and Jeremy Avigad are working on an end-to-end verification of the resolution of Keller's conjecture.
  • Wojciech Nawrocki has been working with Edward Ayers and Gabriel Ebner on widgets for Lean 4, a powerful and flexible framework for supporting user interactions with a proof assistant.
  • Carneiro, Nawrocki, and James Gallicchio have been working on Lean 4's standard library. They have verified properties of hashmaps in particular.
  • Randy Bryant, Nawrocki, Avigad, and Heule have developed a framework for verifying knowledge compilation and model counting, and have written a verified checker in Lean.
  • James Gallicchio has implemented connections between Lean 4 and SAT solvers.
  • Nawrocki is exploring ways to improve the performance of proof assistants based on dependent type theory.
  • Carneiro has reimplemented Mizar in Rust.
  • Undergraduate student Zachary Battleman is working on a framework for verifying for loops and while loops in Lean 4.
  • Patrick Massot is visiting Carnegie Mellon and the Hoskinson Center for the 2023-24 academic year, and he will teach a course on interactive theorem proving.
  • Avigad and Massot have ported Mathematics in Lean to Lean 4 and will continue to expand and improve it.

  • Alexander Bentkamp, Ramon Fernández Mir, and Avigad have been working on verified reductions for convex optimization.

  • Avigad is working with Clive Newstead on developing means for using Lean in an introduction to mathematical proof at Carnegie Mellon.
  • Sean Welleck, who is interested applications of large-language models to formal method and formalization of mathematics, will be joining the Language Technologies Institute at Carnegie Mellon in January 2024.
  • Jure Taslak, a PhD student of Andrej Bauer, is visiting the Hoskinson Center on a Fullbright Fellowship for the 2023-24 academic year, to work on applications of type theory and formal methods to combinatorics.