Math, Inc.
Autoformalization research lab targeting formal verification at scale. Their agent Gauss, integrated with the Lean theorem prover, converts natural language math into machine-checkable proofs; it completed Terry Tao's Strong Prime Number Theorem project in 3 weeks, a task where human experts stalled for 18 months.