Appears he recently raised $120M for this startup which seems quite a large sum for a mathematics startup... curious how investors expect to get their money back.
Off the top of my mind, two possible sources for a finite1 valuation are the possibility of getting acquired for the technology, and the possibility of selling a service that is used by customers who value mathematical rigor [e.g. aerospace engineers]. I agree that $120M is a lot, especially given how rapidly any bored undergraduate from almost any STEM field could vibe code a theorem proving agent as a semester project by gluing together open source tools.
Footnotes