It should be noted that this is a PR piece for a "math" startup. The result doesn't look particularly interesting, from either a mathematical or Lean code standpoint, as far as I can see.
ryandamm 3 days ago [-]
Curious if the authors are hanging around here and how they feel about the recent Leiden Statement. (Late in the article it’s clear that this is at least partially a publicity effort around a new AI math tool, if I’m reading it correctly.)
On a personal level I’m very excited about AI getting good at math, but I’m a consumer of math, not a creator. My job gets easier as AI gets better on this front, so I can’t fully empathize with mathematicians who feel threatened or are worried about the sanctity of the discipline.
black_knight 3 days ago [-]
I am a producer of math. But I feel two ways about AI math.
First I fear slop-math. People producing LLM “proofs” and prose with no value. I do not want to review something the author has spend lies energy on than I will spend reviewing.
Two, I am excited about formal machine-checked proofs. I love formalisation, and if the llm can prove my lemmas I will be a happy camper!
I think my optimism here is coloured by the fact that I am a theory builder, not a problem solver. I will be happy to create beautiful theory, writing (myself) wonderful articles explaining them, but letting the ugly details be formally verified by an LLM.
A problem solver kind of mathematician might feel cheated of all the fun of the llm did all the problem solving.
2 days ago [-]
Rendered at 11:20:35 GMT+0000 (Coordinated Universal Time) with Vercel.
On a personal level I’m very excited about AI getting good at math, but I’m a consumer of math, not a creator. My job gets easier as AI gets better on this front, so I can’t fully empathize with mathematicians who feel threatened or are worried about the sanctity of the discipline.
First I fear slop-math. People producing LLM “proofs” and prose with no value. I do not want to review something the author has spend lies energy on than I will spend reviewing.
Two, I am excited about formal machine-checked proofs. I love formalisation, and if the llm can prove my lemmas I will be a happy camper!
I think my optimism here is coloured by the fact that I am a theory builder, not a problem solver. I will be happy to create beautiful theory, writing (myself) wonderful articles explaining them, but letting the ugly details be formally verified by an LLM.
A problem solver kind of mathematician might feel cheated of all the fun of the llm did all the problem solving.