formal-proofs 开源项目推荐（94 个）

leanprover-community /mathlib3

Lean 3 已废弃的数学组成部分库：请使用 mathlib4

niltok /magic-in-ten-mins

十分钟魔法练习

statebox /idris-ct

formally verified category theory library

LogicalAtomist /principia-rewrite

The Principia Rewrite

mo271 /FormalBook

Formalizing "Proofs from THE BOOK"

rocq-community /hydra-battles

Kirby和Paris的Hydra战斗和Coq中其他有趣数学的变体（协作、记录、包括练习）[maintainer=@Casteran]

data61 /PSL

该项目在 GitHub 上没有填写描述

aripiprazole /rinha

🧪 | Rinha de Backend Lean4

duckki /quantum-computing-lean

Formalized quantum computing in Lean theorem prover

Gbury /archsat

A proof-producing SMT/McSat solver, handling polymorphic first-order logic, and using an SMT/McSat core extended using Tableaux, Superposition and Rewriting.

expln /metamath-lamp

Metamath-lamp (Lite Assistant for Metamath Proofs) is a GUI-based proof assistant for creating formal mathematical proofs in Metamath that does not require installation (just run it directly using your web browser).

RiccardoBiosas /LeanGPT

Experiments with interactive theorem provers, LLMs and formal systems

MixedMatched /juniper

A toy formally-specified Computer Algebra library written in Rust and formalized in Lean 4

Matafou /LibHyps

A Coq library providing tactics to deal with hypothesis

SKolodynski /IsarMathLib

IsarMathLib is a library of formalized mathematics for Isabelle/ZF.

appliedfm /vstyle

A style guide for Coq

pitmonticone /LeanInVienna2024

Repository hosting resources for the "Lean Tutorial in Vienna" at TU Wien from September 18 to 20, 2024.

Looted /kibi

Kibi is a requirement-conformance layer for AI coding agents that keeps product intent connected to code and tests, and catches when implementations drift from it.

xamidi /logic-structuralizer

该项目在 GitHub 上没有填写描述

pitmonticone /FLT3

A formalised proof of Fermat's Last Theorem for exponent 3 in the Lean proof assistant.