STARTUP
Mathematicians and engineers, building AI you can verify.
We're a small, tight-knit team of olympiad mathematicians, quants and engineers, with people who previously worked at OpenAI and Harmonic. We hold AI to the standard of a proof: Midas finds what breaks, fixes it, and checks that the fix holds.
The record so far
6 / 6
IMO 2026 problems solved by Midas Prover, every proof machine-checked in Lean 4
672 / 672
PutnamBench problems proved, including 346 where the answer itself had to be found
18
IMO medals across the team, including multiple golds
5
Major vendors whose software we've found bugs in: NVIDIA, Meta, Google, Intel and Microsoft