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.
alt Hacker News
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.