ProofAtlas

A Lean 4 library that turns formal proofs into computable mathematical objects.

White Paper · Contributing

Status

Main branch contains the design specification for the proof hypergraph. Implementation is on the development branch and will be promoted here as it reaches production quality.

Build

cd lean
lake build

License

Apache 2.0 (see LICENSE).