Dan Abramov’s account of how he used LLMs to do novel math is interesting and revealing. It is possible to deploy these tools to do new and original things, but right now it takes a lot of time, persistence and expertise.
After the way OpenAI behaved here with this math proof, I don’t see how anybody would trust them with secret information. It feels like we haven’t seen the last of this issue yet.
“My expectation is surely in 20 years we are going to see AI tools generating mathematics that in many measurable ways are better than every human mathematician,” Litt said. “I would be shocked if that doesn’t happen.”
“This amazing snippet of code was languishing in the docs of dead software, which in turn the original formula was scrawled away in a math textbook from the 60s.”
Good to have explained this explicitly why mathematics is such an essential component of programming. People without an inclination for this kind of abstract mathematical thinking often are poor and chaotic programmers.
A very cool and simple introduction into Lean and what makes it interesting. I’m not sure exactly what draws people in this direction but it’s cool to see the progress that’s being made here.
Solvers are very annoying to setup and plug your problem into if you’re using them regularly. That’s why hooking them into LLMs to do the annoying manipulation work is an amazing idea.