Proof-related projects

To contribute to the web site, please open an issue, create a pull request or send a mail to the science communication coordinators.

• 2024-2029: CertiFOX, Certified First-Order Model Expansion

• 2024-2027: APPAM: proof assistants for learning mathematics

• 2022-2026: ForCUTT, Formalisation of Constructive Univalent Type Theory (ERC Advanced Grant to Thierry Coquand)

• 2022-2025: ICSPA, Interoperable and Confident Set-based Proof Assistants

• 2021- : Hoskinson Center for Formal Mathematics [news]

• 2021-2026: Type Theory for Mathematics and Computer Science

• 2020-2025: TydiForm: Type Theory for Data-Intensive Formalization

• 2021-2024: LISA: Proof assistant based on set theory

• 2017-2022: Alexandria, Large-Scale Formal Proof for the Working Mathematician

• 2017-2022: SMART, Strong Modular Proof Assistance Reasoning Across Theories

Smaller projects

• 2023: after her STSM, Dragana Milovancevic (EPFL, Switzerland) received a 6-months Doctoral Mobility Grant from the EPFL to continue her collaboration with Carsten Fuhs (University of London, UK).