PatrickMassotcheckdecls

Tiny Lean library to check existence of declarations
Displaying 1-20 of 90 packages depending on PatrickMassot/checkdecls
Sort by

  1. b-mehta/ABCExceptionsuseslean4.18.0

    Exceptions to the ABC conjecture in Lean

  2. mbrcic/ai-safety-formalization-atlasuseslean4.18.0

    The open workbench for AI safety, made formal. Turn safety questions into machine-checked Lean proofs — a shared launchpad where researchers and AI agents build provable safety together.

  3. cslib-community/AlgoLibuseslean4.18.0

    This is the repository for algorithm design.

  4. YaelDillies/APAPuseslean4.18.0

    Formalisation of the Kelley-Meka bound on Roth numbers

  5. mo271/Aperyuseslean4.18.0

  6. Verified-zkEVM/Arklibuseslean4.18.0

    Formally Verified Arguments of Knowledge in Lean

  7. JobPetrovcic/ArtinWedderburnuses11fa569

    A formalized proof of Artin-Wedderburn theorem in Lean4

  8. fpvandoorn/bonnAnalysisuses21a36f3

    repository for the collaborative formalization seminar in Analysis in Bonn

  9. Whysoserioushah/BrauerGroupuseslean4.18.0

  10. RemyDegenne/BrownianMotionuseslean4.18.0

    Construction of a Brownian Motion in Lean

  11. RikHeurter/BscThesisFormalisationuseslean4.18.0

  12. amellendijk/BVuseslean4.18.0

    A Lean blueprint documenting a formalization of Bombieri-Vinogradov

  13. fpvandoorn/carlesonuseslean4.18.0

    A formalized proof of Carleson's theorem in Lean

  14. YaelDillies/ChandraFurstLiptonuseslean4.18.0

    Formalisation in the Lean theorem prover of the relation between corner-free sets and communication complexity

  15. kbuzzard/ClassFieldTheoryuseslean4.18.0

    Github repository for the 2025 Clay Summer School on Formalizing Class Field Theory

  16. mccorvie/ClassificationOfSurfacesuseslean4.18.0

  17. RemyDegenne/cltuseslean4.18.0

    Central limit theorem in Lean

  18. teorth/equational_theoriesuseslean4.18.0

    A project to map out the relations between different equational theories of Magmas.

  19. kim-em/ErdosUnitDistanceuseslean4.18.0

    Formalization of Alpöge's disproof of the uniform-constant Erdős unit-distance conjecture (companion to mathlib4 branch kim/erdos-unit-distance)

  20. kim-em/ErdosUnitDistanceComparatoruseslean4.18.0

    Independent comparator verification: the uniform-constant Erdős unit-distance conjecture is false (Alpöge 2026, formalized)