Imagine you were a programmer in the 1950s. Your day to day was punching machine code into cards.

In the 1970s, you were wrestling with FORTRAN. By the 1990s, maybe C++. Today? You're basically just talking to the computer in English. Turing's childhood dream is now your reality with coding agents.

Each generation got to think a little less about the machine and a little more about the fun problem they were actually trying to solve.

Modern compilers are one-way DAGs. They take Python and transform it down the stack through multiple representations until it becomes machine code. There's some upward flow - as you type in your IDE, a partial compilation happens via Language Server Protocol, feeding information back up to create those squiggly lines and suggestions. But compilers never go fully back up the abstraction ladder. Disassembly exists, but it doesn't reconstruct your original high-level intent.

Mathematics needs something compilers never achieved: a true bidirectional cycle. For thousands of years, mathematicians think in high-level, intuitive leaps, not formal logic. Yet, math is undergoing a modernization. With proofs now spanning hundreds of pages, they are often riddled with hidden errors. In fact, every time proofs dogmatically resist being formally proven, the informal human source was wrong – just recently, mistakes were fixed during the formalization effort of Fermat's Last Theorem. The bottom formal layer catches what high-level intuition misses.

Meanwhile, autoformalization - the process of converting natural language proofs to Lean code - is a form of hierarchical planning, bridging between the abstraction layers.

Going down the stack: Autoformalization translates intuitive mathematical reasoning into formal proof – the compiler's traditional direction.

Going up the stack: Autoinformalization translates formal proofs back into human intuition – something compilers never truly do.

When combined, these create an interactive prover in natural language, freeing mathematicians to explore dozens of strategies and rapidly prototype ideas while the machine handles formalization.

But here's the most powerful part: machine discoveries at the formal level feed back up. The machine finds patterns, lemmas, and connections in the formal space that humans never intuited, then surfaces them as new high-level insights. The mathematician's intuition becomes augmented by discoveries happening in a space they couldn't naturally explore.

The compiler revolution took decades; the mathematical compiler revolution is happening now.

You are a gold prospector in 1849. Everyone brings you shiny rocks claiming they've struck it rich.

Experienced prospectors examine them: "Looks like gold to me."

But when confronted with exotic ores, even experts disagree. Their pattern matching fails on things they've never seen.

Then someone brings an assayer's scale. The metal either dissolves in acid or it doesn't. Binary truth.

When you write a proof, it's either correct or it's not. Formal verifiers like Lean provide perfect ground truth while model judges are pattern matchers that fail when being pushed on generating genuinely novel proofs. From an engineering angle, verification gives us efficiently scalable rewards for learning.

And here's the philosophical perspective of why we need formal verification: Our self-consistent, observer-supporting universe follows rules that can be captured mathematically – from laws of physics to probability theory. Mathematics is the consistent language of our consistent universe and formal languages like Lean let us consistently operate in the mathematical world model.

We are training systems in mathematics as reality's minimal simulation – by learning to navigate the world of mathematics one grounded step at a time, the hope is that the AI has learned some fundamental rules that our reality has to follow. Video generation models learn physics too. Sometimes one ponders … where do abstract reasoning and spatial reasoning join?

While able to test if gold is real, finding new veins is harder: working in concert with verification, we enter the chapter of scientific discovery. Imagine you're in the middle of an ocean. Sailing towards new lands, of course, you start daydreaming about mathematics:

Your map is the Knowledge Base – showing where you've been. The entire corpus of mathematics indexed into a knowledge graph: definitions, theorems, and proofs. Formalized mathematics as a searchable, Internet-scale dataset.

Your ship is the Conjecturer – navigating uncharted territories. It spots distant landmasses through fog: "something valuable three days west." Built for open-ended exploration beyond known results, it samples out of distribution and generalizes with leaps guided by intrinsic motivations.

But when you spot an unknown island on the horizon, how do you know if it's India or the West Indies? The shape looks right, the distance seems plausible, but educated guess isn't certainty. You ask the experienced captain for wisdom that you trust – that is the Prover. Successful proofs extend the knowledge base. Failed attempts provide signals for improving both the Conjecturer and Prover. While formal verification turns "might be true" into "is true," counterexample construction shows "is false." Both grow the library.

The loop is self-reinforcing. More verified theorems mean a richer knowledge base. A richer knowledge base enables more sophisticated conjectures. More proof attempts (successful and failed) train better models. Better models generate more interesting conjectures and find proofs faster.

Axiom is building the AlphaGo for mathematics, but with infinite branching.