The AI industry learned to generate. The next leap is learning to prove. A 25-year-old mathematician is betting $1.6 billion on the gap between the two.
Thanks, I was meaning to find out more about this company. I don’t know Lean well but I always assumed that if it’s like any other programming language, the key is that it is generative. As in, you have primitives and operators and can start just combining them to generate new things. In lean’s case those may become new lemmas or theorems, which are potentially more useful than an LLM just generating a novel. Additionally, like I wrote about in the context of robotics, I’m a big believer in the pairing of language models with tools, so I’m looking forward to seeing what comes of this!
Yes. It’s a uniquely compelling company. You can follow their founder, Carina Hong (@CarinaLHong), and Founding Mathematician Ken Ono (@KenOno691) on X to stay close to how it unfolds.
Thanks, I was meaning to find out more about this company. I don’t know Lean well but I always assumed that if it’s like any other programming language, the key is that it is generative. As in, you have primitives and operators and can start just combining them to generate new things. In lean’s case those may become new lemmas or theorems, which are potentially more useful than an LLM just generating a novel. Additionally, like I wrote about in the context of robotics, I’m a big believer in the pairing of language models with tools, so I’m looking forward to seeing what comes of this!
Yes. It’s a uniquely compelling company. You can follow their founder, Carina Hong (@CarinaLHong), and Founding Mathematician Ken Ono (@KenOno691) on X to stay close to how it unfolds.