American AI startup working on automated mathematical proof verification. Its bot, Aristotle, verifies proofs by first translating them into a rigorous language of symbols and axioms, making use of Lean, an open-source coding language popular with mathematicians. When a human proof-writer has made small errors, Aristotle attempts to fix them; when the human has skipped steps—mathematicians often make intuitive leaps—it fills in the details. The result is an airtight proof that follows the same principles as the original. Tudor Achim is the company's boss.
I can't understand why people are frightened of new ideas. I'm frightened of the old ones.