Relying on GPT style systems to translate high level math to lean stuff strikes me as dangerous unless you're going to double-check by hand that the LLM didn't suddenly decide to hallucinate parts of the answer.
Granted, the hallucinated part might not pass the final Lean verification, but ... what if it does because the LLM did not properly translate the mathematician's intent to Lean language?
I'm thinking the human will still need to read the Lean program, understand it and double-check that his original human intent was properly codified.
Better than having to produce it by hand, but still sub-optimal.
Granted, the hallucinated part might not pass the final Lean verification, but ... what if it does because the LLM did not properly translate the mathematician's intent to Lean language?
I'm thinking the human will still need to read the Lean program, understand it and double-check that his original human intent was properly codified.
Better than having to produce it by hand, but still sub-optimal.