ProofLens and Viridis Canon: open Lean 4 projects seeking users and reproducibility feedback

[jdhart81]

ProofLens and Viridis Canon are two public Lean 4 projects I maintain. Both code repositories are open source under Apache-2.0, and I’m inviting Lean users, educators, and researchers to try them and report what works or fails.

ProofLens: see what a Lean statement means

ProofLens turns supported Lean conjectures and theorems into visual explanations of their objects, relationships, and assumptions. The browser now accepts pasted declarations, .lean files, and extracted Formal IR JSON. Supported real-arithmetic statements have interactive plots and downloadable explanations and SVG charts.

• Try the browser app
• Bring your own statement or run local Lean extraction
• Report an unsupported or confusing example

The source preview supports a limited subset of Lean syntax and mathematics. It does not run Lean or verify proofs. Imported JSON metadata does not establish verification, and a plotted example does not prove a general statement. Those boundaries remain visible in the output.

Viridis Canon: inspect and reproduce conditional mathematics

Viridis Canon publishes Lean source and research artifacts studying connections among information, thermodynamics, learning, and living systems. It includes pinned reproduction instructions, axiom audits, and a claims matrix that distinguishes formal strength, assumptions, and quarantined results.

• Browse the research catalog
• Read the exact claims and caveats
• Reproduce the builds
• Report a reproduction, critique, or assumption challenge

Lean checks what follows from the stated definitions and hypotheses. It does not establish that those assumptions describe nature. Formal verification, empirical validation, and independent peer assessment are separate. Viridis discloses its automated proving and drafting tools in AI use and authorship; I remain responsible for the released claims. Research records carry their own licenses.

A useful first contribution

For ProofLens, try one statement from your own project and tell us what the visualization helped you understand—or share the smallest example that confused it. For Viridis, reproduce one build or challenge one specific hypothesis or formalization. Please include the exact declaration or artifact, revision, environment, and observed result. Failed reproductions and substantive criticism are welcome.

— Justin Hart

[jdhart81]

Try ProofLens on a statement you want to understand

I've published a builder-use example and documentation recipe with an actual browser-exported chart and reproducible CLI figures.

If you're writing Lean theorem documentation or a teaching example, try one small public or synthetic statement from your own work:

1. Open ProofLens, choose Explore your own Lean, and visualize a supported statement. No installation, account or payment is needed to try the browser.
2. Check the assumptions and keep the proof-status qualifications visible. Source preview does not run Lean; an input using sorry remains unproved, and numerical charts are not proofs.
3. Save a chart/explanation and see whether it helps explain your theorem to another reader. The packet includes a plain HTML companion-page recipe. For leanblueprint projects this is a manual linked companion, not a plugin or tested build integration.

I'd welcome one concrete result: what question you had, what became clearer, or the first blocker. Reply here or use the first-use report. Public or synthetic examples only; no contact details or private research needed. Participation is optional, and a precise failure is useful feedback. I'll ask separately before using anyone's words in a showcase.

The examples were tested by the maintainer on October 12; they do not establish outside adoption. The next improvement will follow a demonstrated builder need. If the output belongs naturally in an existing project, we can scope a small integration together before changing that project's tooling.