M
Math Inc.
Emerging neolabBuilds AI agents that formalize mathematics and software into machine-checkable proofs in Lean
Raised, confirmed—0 confirmed rounds
Valuation, confirmed—none disclosed
Valuation, reported—no open report
Founded2025San Francisco, CA, US
Key facts
| Field | Value | Source · checked |
|---|---|---|
| Classification | Emerging neolabAutoformalization research company building the Gauss agent; backed by Hack VC (2026) | |
| Field | AGI and superintelligence | |
| Founded | 2025 | scientificamerican.com helped launch the start-up Math, Inc., in the late summer of 2025checked 15 Nov 2026 |
| Headquarters | San Francisco, CA, USAuthor affiliation of Math, Inc. in an arXiv paper (Progress in Formalizing Sphere Packing in Dimension 8). | arxiv.orgchecked 15 Nov 2026 |
| Founders | Jesse Han, Christian Szegedy | |
| Website | math.inc | |
| Careers | math.inc | math.incchecked 15 Nov 2026 |
| Profiles and work | X @mathematics_incGitHub, 9 public repos | How links are checkedchecked 15 Nov 2026 |
Funding rounds
No round of Math Inc. is confirmed by the company or a regulator. Rounds marked Reported or Abandoned are not included in that total. Status rules: methodology.
| Date | Round | Amount | Valuation | Investors | Status | Source · checked |
|---|---|---|---|---|---|---|
| 18 Jun 2026 | Funding round | undisclosed | — | Hack VC | Reported | Hack VC We invested in Math Inc. because we think the answer to that question becomes core infrastructure for an increasingly AI-driven worldchecked 9 Nov 2026 |
Notes on these rounds
- 18 Jun 2026 Funding round: Investor states it invested; round type, amount and co-investors not disclosed.
People
| Name | Role | Before | Now | Source · checked |
|---|---|---|---|---|
| Jesse HanXLinkedInSite | Co-founder & CEO | OpenAI (Senior Research Scientist) | Current | |
| Christian SzegedyLinkedIn | Co-founder | — | Current | |
| Jared Duker LichtmanScholarSite | Member of the team | Stanford (NSF Postdoctoral Fellow) | Current |
Professional facts from public sources only. How people records are handled.
What it has shipped
| Name | Kind | Date | Open weights | Source · checked |
|---|---|---|---|---|
| Gauss | product | Sep 2025 | No | math.inc Using Gauss we produced ~25,000 lines of Lean code, comprising over 1,000 theorems and definitions.checked 9 Nov 2026 |
| OpenGauss | tool | Yes | math.inc OpenGauss is a state-of-the-art open-source autoformalization harness for Lean.checked 9 Nov 2026 |
Work at Math Inc., or see something wrong? Update this profile with a public source. How corrections work.