Reasoning is transparent
Publish your ideas in a form that showcases their logical structure. Leave concepts opaque when you need to — but the reasoning that connects them must be explicit.
Now in Early Access
Make your ideas precise enough to be proven wrong.
Axiom is an ecosystem rooted in formal logic. It ensures that conclusions follow from their premises. Refine your ideas, publish statements, and adopt or reject claims.
Who decides what's true? You do. Axiom ensures arguments are valid — your premises decide what is true.
From the founders
Introduction & Walkthrough
Online arguments don't resolve — they dissolve. Definitions drift, goalposts move, both sides declare victory. We built Axiom so arguments can actually be lost. Give us 5 minutes, and we'll show you how.
THE AXIOM PLATFORM
An Arena for Ideas
Axiom's shared knowledge graph is where ideas compete in the open. Every argument carries a machine-checked proof, consequences can't be ignored, and positions that lead to contradiction drop out of the discourse. Anyone can inspect the public reasoning. Learn more.
Illustrative animation, not real Axiom data.
Logic is the referee
Your argument stands only when a Lean 4 proof connects it to stated premises. Who you are never matters — only whether the proof checks.
Positions are public
Every stance you publish builds your world model. You formally adopt or reject ideas, and your profile shows exactly what you hold, and why.
Consequences propagate
Anyone's proof can connect your commitments to conclusions you never anticipated — even a contradiction, which locks you out of publishing until you publish a revision.
Why express ideas in code?
The exponential payoff
It's more than a technical preference; it's how Axiom guarantees transparent and precise thinking.
The Exponential Payoff
Higher quality contentWhen everything must logically follow, it raises the standard of discourse.
From narratives to proofProofs aren't valid because of status or rhetoric. They are valid because they are mathematically correct—and get rejected when they aren't.
EfficiencyEvery time you interact with any statement, you reap the benefits of knowing that it inherently follows from its premises. Automatic verification is not a one-time benefit—it compounds.
TransparencyWhen you are required to map out your reasoning, the incentives change. It's an opt-in paradigm shift you can't match anywhere else.
Surface hidden assumptionsTraceability allows you to examine your core assumptions so you can ask “wait, why are we assuming this premise is true in the first place?”
Richer understandingWhen the entire chain of reasoning is accessible, you can explore the precise depth of complexity that suits you.
Fixed goalpostsThe antidote to gaslighting.
Common groundAn undefined conflict cannot be effectively resolved through undefined actions or unbounded terminology. Using fixed definitions allows the problem space to be narrowed and traced to the root disagreement—the last point of common ground. It turns chaos into something we can articulate.
Unlocked complexityYou can explore far more complex logical conclusions when each logical step is proven, traceable, and fixed. With each iteration, you can choose exactly how to branch—like a fractal.
✓
Axiom's Conclusion
When we try to solve hyper-complex global challenges using untraceable, shifty language, we hit a ceiling. Axiom lets our reasoning scale.
See our Article: Reality Can Be Modeled
Roadmap
We're just getting started
Axiom is in early access. We're shipping new features every week as we build towards our much larger vision.
Current Phase
Early Access
Designed to get the core logic into the hands of early adopters. Expect missing features, rough edges, and the opportunity to play an important role helping shape how Axiom evolves.
Launch & Beyond
The Bigger Vision
What you see today is just the beginning; we have concrete plans for much more. When ideas are expressed in logic, the possibilities are awesome! Read more.
Public Roadmap
We're putting together a public roadmap with the specifics — what's shipping next and the concrete vision beyond early access. We will share it as soon as it's ready.
FAQ
Absolutely not. If you are comfortable expressing logical rules (e.g., "If it rains, my clothes will get wet; therefore, I need an umbrella"), you already understand logic. Axiom is designed to help you organize and refine those thoughts without needing advanced math knowledge.
Still not comfortable? No problem. Our AI skills library is designed to ask you illuminating questions that hold you to a much higher standard of thinking no matter your starting point.
While our thesis is that code is required to effectively reason through many of humanity's ongoing and upcoming issues, Axiom's integrated AI will adapt to meet you where you are and answer any questions about the Lean code you write. Even a beginner who has never heard of Lean or seen a ∀ before can absolutely still use Axiom.
Still unsure? Our Discord is full of people excited to help you learn!
Axiom uses Lean 4, one of the most popular languages for expressing math in code. By using Lean 4 as its base, Axiom benefits from the rich ecosystem of formalized concepts and all the impressive work in Lean auto-formalization.
Our goal during early access is to share this new technology as soon as possible. Therefore, users during early access will need to have some technical experience downloading and using their own AI agent.
At launch our goal is to remove much of this friction and setup. Eventually, our goal is to make Axiom a valuable product to users of all ages.
You can set up Axiom, formalize and check ideas locally, browse public arguments, and build on their Lean code for free. An Axiom platform plan is required when you want to publish your work, take public positions, use default server-side checking, or participate in the early-access community.
From philosophy, policy, and morality to math, research, and conspiracy theories—the only requirement is logical validity.
While you can post about any topic, it's unlikely that you will end up making confused criticisms or hasty hot takes. Axiom is built for thoughtful discourse and higher quality reasoning.
You will need to bring your own AI agent and follow the guided setup for your local Axiom workspace. Claude, Codex, Cursor, Gemini, and Copilot are supported, and you do not need an Axiom platform plan to begin.
Yes. Your Lean files stay local, belong to you, and can be used independently of the Axiom platform.
We don't. You can absolutely have subjective premises and have subjective conclusions. We simply enforce that your logic is valid and any known contradictions are addressed.
Your next move
Start with an idea. Share it when it's ready.
Reason privately for as long as you need, then contribute your work to a public body of knowledge.
01 · Refine
Start with an idea
Make your assumptions explicit, test the edges, and build on public Lean code for free.
Get started free02 · Contribute
Share it publicly
Publish your reasoning, invite thoughtful challenge, and give others a foundation they can build on.
View Axiom plans