Visual manual
Constructor fields, scope links, folds and typing rules. Four interactive examples show how the representation works.
Proof Atlas
A geometric language for Lean proofs
The program studies how a fixed visual vocabulary can represent proof structure, binding and typed constructions, including large AI-generated proofs. Every source object keeps its exact compiled identity. Begin with the notation, then inspect a recorded proof.
The Riccati bound
Follow a compiled proof through its original occurrences, local context and recorded native judgments. The complete library is available in the same reader.
Research program
The questions, current capabilities and unresolved gaps. The evidence index groups detailed checks by research layer.
Established structural result
The two project snapshots contain 739 and 1,359 declarations. In the working corpus, 670,018,056 expanded expression occurrences are represented by 1,277,896 shared nodes, retaining ordered children, payloads and contextual binding.
Exact structure and bounded navigation are supported by finite audits. General semantic compression and improved human comprehension remain unmeasured.
Applications and reference
The SE(2) article reader synchronizes prose, compiled Lean and graph selections. Precise proof-step matches and broader context are labelled separately. Five numbered article statements have partial, conditional counterparts; four remain unformalized.