01∅
Start from zero
Make axioms, rules, and dependencies explicit. Build knowledge from a minimal formal foundation, with a traceable path for every result.
AN OPEN AI FOR MATH PROJECT
From first principles.
Let mathematics
grow on its own.
Building toward autonomous mathematics, from the ground up.
AI explores the proof. Every step can be checked.
+A minimal beginning. An open horizon.
A traceable path of reasoningFIG. 001
Every conclusion has a path back to its foundations.
∅Built from zero↗Autonomous exploration⊢Independent verification∀Open collaboration
01 / OUR VISION
The next chapter of math.
Written by reasoning.
We believe mathematics can grow in a new way.
Our long-term goal is a mathematical system that develops without relying on human mathematicians. Starting with explicit axioms and inference rules, AI would propose definitions, explore statements, and produce proofs for an independent verifier to check, step by step.
No human endorsement should be needed for each result. Everyone should be able to inspect, reproduce, and help build the system.
02⊢
Make proofs verifiable
A plausible answer needs an explicit proof. Every inference should be open to independent checking and replay.
03∀
Keep mathematics open
Open code, open rules, open discussion. Math enthusiasts, researchers, and developers all have a place to contribute.
02 / HOW THE SYSTEM GROWS
Explore freely.
Verify rigorously.
Producing a proof and checking it are separate jobs.
AI can explore boldly. Results must follow explicit rules.
⊙01→
THE FOUNDATION
Axioms & rules
Publish the assumptions, definitions, and inference rules.
↗02→
AUTONOMY · OUR GOAL
AI exploration
Explore statements and construct explicit proof certificates.
≡03→
THE RECORD
Proof certificates
Record each conclusion, inference rule, and dependency.
✓04
THE CHECK
Independent replay
Check every step against a selected claim and its premises.
Trust grows from open rules and reproducible checks.
Read the specification03 / A PROOF YOU CAN INSPECT
Go beyond the conclusion.
Check every step.
Choose a statement and replay its derivation.
Try altering a step. See what the checker has to say.
STATEMENT TO CHECK
P → P
Assume P, then discharge the assumption to derive that P implies P.
| Step | Conclusion | Inference rule | |
|---|---|---|---|
| 01 | P | Assumption | · |
| 02 | P → P | Implication introduction | · |
The last rule is replaced with conjunction elimination. The selected claim stays the same.
Inspect certificate JSON+
{
"format": "lemqo-proof-v1",
"logic": "ipl",
"formulas": [
[
"atom",
"P"
],
[
"imp",
0,
0
]
],
"steps": [
[
"assume",
0
],
[
"imp_intro",
1,
0
]
],
"root": 1
}This demo replays propositional-logic examples from the repository. Use the open-source verifier for full verification and input checks.
Run it locally04 / FROM TODAY TO TOMORROW
An ambitious direction.
An auditable beginning.
Autonomous mathematics is our long-term vision.
Today, we begin with transparent proof verification.
CURRENT RELEASE · v0.2
First, make verification solid.
Propositional-logic kernel
10 fixed natural-deduction rules for implication, conjunction, disjunction, and falsehood.
Read the specificationExperimental Lean certificates
3 selected main theorems in a restricted corpus have independent check records. This path remains experimental.
Inspect verification recordsNEXT · RESEARCH DIRECTIONS
Strengthen the foundations of trust.
Read the full roadmap05 / BUILD FROM ZERO, TOGETHER
Mathematics belongs
to the curious.
Math enthusiasts, mathematicians, AI researchers, developers.
Bring your curiosity. Help turn ideas into verifiable reasoning.
Explore mathematics
Run examples, ask questions, and share statements you want to explore.
Study reasoning
Review axioms and rules. Research assurance and formal expression.
Build the tools
Improve checkers, tools, documentation, and the experience of working openly.