4 ms·

If it's just a hobby, why would you use an LLM at all?

• black_knight 2mo ago
  It is not a hobby when you are paid to do it! But I take it you mean “Done for the art of it”. Which I guess is a concept foreign to many. A few different reasons why use an LLM when mathematics is done for its own sake: Formally verifying my proofs catches any mistakes I make, but verifying is also hard work. LLMs shaves off a lot of time when formally verifying a proof. I can still read through an LLM generated proof and understand it. This is a way for me to understand the result I am working on (usually in order to know what to prove next, results are not proven in a vacuum). My experience thus far is that, while correct, an LLM generated proof is often unnecessarily complicated or inelegant. I take pleasure in elegant proofs and will spend time iterating on the first proof until I find it conveys the idea in the most elegant way. Having the initial LLM proof to start with is really useful, but is thus far rarely the final product.