Why We Invested in Math Inc.

By: Harrison Dahme

Solve math, solve everything.

Mathematics is the purest form of elegance we have - the one language in which a claim can be made true beyond doubt. Everything that must not fail eventually reduces to it: a settlement that has to clear, a kernel that cannot be exploited, a proof that has to hold. Physics, biology, chemistry, software are all flavours of applied math. In the case of software, some combination of the human and the compiler evaluate correctness. For decades that was a fair trade, because humans wrote the software and humans, slowly, could reason about it.

AI breaks that trade. As machines write most of the world's code, proofs, and decisions, generation stops being scarce, and correctness becomes the bottleneck. The question is no longer "can we produce it?" but "can we prove it's correct?" We invested in Math Inc. because we think the answer to that question becomes core infrastructure for an increasingly AI-driven world - and because Math is the team to build it.

What Math Inc. Is Building

Math's thesis collapses to one line: wherever software must not fail, a proof is the product. The company is building industrial-grade autoformalization - AI agents integrated with theorem provers like Lean that take messy, real-world inputs and turn them into machine-checkable proofs. Ingest the source material, infer the spec, prove it correct, and verifiably compile down to the binary that actually ships. The proof travels all the way from the intent of the code to the metal and sand it actually runs on.

Their flagship agent, Gauss, has already crossed a threshold no one else has. It autonomously synthesized a formalization of the sphere, packing results in dimensions 8 and 24 (roughly 200,000 lines) in three weeks of compute, with no humans in the loop. It is the largest singular autoformalization result ever created. For context, the 8-dimensional case alone took a team of more than seven people six months to formalize by hand, and that was only a third of the problem. The 24-dimensional case is far harder. Gauss did the whole thing autonomously in an eighth of the time.

What makes this more than an academic trophy is the trajectory and acceleration of complexity:

• June 2025: 3,500 lines (de Bruijn's theorem on the ABC conjecture), in three weeks
• September 2025: 25,000 lines (Strong Prime Number Theorem), in three weeks
• February 2026: 200,000 lines (sphere packing in 8D and 24D), in three weeks

The order of magnitude grows each time while the wall-clock time stays roughly constant. These milestones are also software milestones in disguise. Solve math, and you have solved the general problem. Every run also extends a proprietary corpus that makes the next agent more capable, further increasing the data flywheel.

Why We Invested

As a crypto native firm, we’re very familiar with domains where correctness is already non-negotiable - code is law, as the refrain goes, settlement is final, and a single bug in a contract or cryptographic primitive is an irreversible, multi-million-dollar event with no rollback.

We've spent years underwriting that risk through audits, economic guarantees, and failsafes. As a firm, we’ve placed many bets in this category, including the seed round of Sui. Sui is instrumental in building MOVE, a language designed with formal verification baked in from the beginning. However formal proofs are the strictly stronger version of the same guarantees, replacing "no one found a bug" with "no bug can exist." The same machinery that lets Gauss prove a theorem is what verifies a ZK circuit, a bridge, or a node client.

This isn't a fringe bet either. The same conversation is now happening in the frontier AI research community. The field's leading labs, mathematicians, and systems researchers are convening around verification as a first-class problem. This might be one of the most powerful mechanisms we have to verify model outputs and internal states, which could make massive strides in alignment research, one of the existential problems of our time. Furthermore;

1. Verification is a derivative of AI capex.

As AI moves from copilot to operator, vibing (and breaking) things in production stops being acceptable for meaningful systems - such as power grids, financial settlement, cryptography, defense infrastructure, autonomous machines, and the AI training and inference stack itself. Formal guarantees become a control layer for anything that depends on software behaving exactly as specified. If output scales nonlinearly and trust does not, correctness becomes the bottleneck. Math is the bet that this bottleneck becomes infrastructure.

2. The team literally created this field.

Autoformalization sits at the intersection of cryptography, machine learning, theorem proving, and pure mathematics - a brutally hard combination to staff. Math has assembled what we believe is the strongest team in the category:

• Jesse Han (CEO) was a Senior Research Scientist at OpenAI, contributed to the GPT-4 Technical Report, and developed GPT-f, the first neural theorem prover whose proofs were accepted by the formal mathematics community. He co-authored the foundational papers in the field - GPT-f, PACT, and miniF2F - led Flypitch (the formalization of the independence of the continuum hypothesis), and completed his PhD under Tom Hales, who led the formal verification of the Kepler conjecture. He helped invent neural theorem proving
• Jared Duker Lichtman, an NSF Postdoctoral Fellow at Stanford, completed his PhD at Oxford under Fields Medalist James Maynard and solved the 30-year-old Erdős primitive set conjecture, a world record in analytic number theory.
• The broader team includes world experts in real-world distributed-systems verification, probabilistic and concurrent C program verification, reinforcement learning for proof compression, cost-efficient zero-knowledge proofs, and the primary maintainers of the leading open-source Lean agent tooling.

Math is also the only company Dr Terence Tao works with. For those unfamiliar, Dr Tao is arguably one of the great mathematicians alive today - as much as one can be a household name, it’s him. Our diligence calls pointed to the same conclusion: Math is world-class at long, complex proofs, and the ability to run for days on mammoth-scale formalizations is a capability its peers simply do not have.

3. The capability gap is real and the advantage grows.

What impressed us most was not any single benchmark but the depth of what Gauss can do. Competition-grade theorem proving - Olympiad-style problems - is increasingly reproducible, and benchmark gains commoditize quickly. Generating six-figure-line formalizations of frontier research over days of compute is qualitatively difficult: it demands large scale formalization, library management, and long-horizon synthesis that is hardest to copy. Each run extends Math's proprietary library, which yields richer training signal, which produces more capable agents, which formalizes harder results.

How We Think About the Market

Two analogues frame the opportunity. Wolfram built a vertically integrated computational stack and monetized it through academic licenses, enterprise subscriptions, and institutional lock-in. Math is going one layer deeper - a verification stack embedded in research labs, critical infrastructure, finance, and AI pipelines.

The public-market comparison we keep returning to is Cadence. Cadence sells the electronic design automation software that verifies chip designs before fabrication, and it has embedded itself so deeply that no chip ships without sign-off. Math is trying to do for AI-generated software what Cadence did for silicon; become the gate everything passes through before deployment. Both sit downstream of enormous CapEx and monetize correctness as a gating function.

The business stays defensible by sharing zero-knowledge proofs which let customers verify a guarantee, without ever seeing the proof code.

We're clear-eyed about the difference from Cadence. Chip verification is mandatory and errors are irreversible; software today can still afford vibing in production, and there is no universal mandate that AI-generated systems be formally verified. Math is betting that verification becomes a norm rather than an option. We share that conviction - but it is the central bet, and we underwrite it as such. The strongest near-term forcing function is the public sector: a soon-to-be-released RAND report frames the scale of required software hardening as comparable to Y2K, carried out primarily by commercial parties. Math is already on the procurement ladder, with early Galois/RAND and DARPA OTA work - the same fast-track vehicle that carried DARPA's HACMS program into $100M+ in downstream contracts for vendors like Anduril, General Atomics, and Tangram.

The Bottom Line

Math is building the verification infrastructure for an AI-native economy. Solve math, and you solve everything downstream of it - the code, the proofs, the cloud, the inference stack, the world's software. If AI-generated output comes to require universal verification layers, and we believe it will, Math is positioned to be the default runtime and governance layer for verified reasoning. The team created the field, the product is shipping results no one else can, and the moat grows with every formalization.

That is a bet we were glad to make early.

Disclosures

The information herein is for general information purposes only and does not, and is not intended to, constitute investment advice and should not be used in the evaluation of any investment decision. Such information should not be relied upon for accounting, legal, tax, business, investment, or other relevant advice. You should consult your own advisers, including your own counsel, for accounting, legal, tax, business, investment, or other relevant advice, including with respect to anything discussed herein.

This post reflects the current opinions of the author(s) and is not made on behalf of Hack VC or its affiliates, including any funds managed by Hack VC, and does not necessarily reflect the opinions of Hack VC, its affiliates, including its general partner affiliates, or any other individuals associated with Hack VC. Certain information contained herein has been obtained from published sources and/or prepared by third parties and in certain cases has not been updated through the date hereof. While such sources are believed to be reliable, neither Hack VC, its affiliates, including its general partner affiliates, or any other individuals associated with Hack VC are making representations as to their accuracy or completeness, and they should not be relied on as such or be the basis for an accounting, legal, tax, business, investment, or other decision. The information herein does not purport to be complete and is subject to change and Hack VC does not have any obligation to update such information or make any notification if such information becomes inaccurate.

Past performance is not necessarily indicative of future results. Any forward-looking statements made herein are based on certain assumptions and analyses made by the author(s) in light of their experience and perception of historical trends, current conditions, and expected future developments, as well as other factors they believe are appropriate under the circumstances. Such statements are not guarantees of future performance and are subject to certain risks, uncertainties, and assumptions that are difficult to predict.