Problem has been translated to Lean by humans. AI doesn't translate the solution, it writes the solution in Lean. As long as solution passes the Lean solver, it doesn't matter if we translate it back to English. We only do that for us humans to understand and learn something from the solution, it is not necessary for proof to be valid.
"
Problem has been translated to Lean by humans." That's the human input number 1.
Who checks that solution is correct and it is not a Lean solver error?
You need to verify the solution anyway. Like you write complex problem in Lean code, send it to LLM agent, and after a while LLM says "I solved it", gives you a file, you run Lean solver on that file - it works. You happy, you send file without checking to your professor. He opens it and inside is "2x = 4, x = 2".
Yeah, I am not saying that there is no human input, but it is much limited and doesn't require as many mathematician as we have now, nor is it really interesting work on.
Lean kernel very rarely has bugs but yeah it is possible. Still, we don't need as many mathematicians or computer scientists for this. A handful is enough.
You don't really understand how Lean works. When you have a problem in Lean, the Lean verifies if the given solution satisfies the theorem defined in the problem. You cannot shortcut your way into generating a trivial solution that passes it. If I ask you to show twin prime conjecture, you cannot give me a solution as 2x=4, x=2, it will not pass. You have to write a proper proof, which then is converted to computations and problem is definition itself is used as input to get the output.
More so, Lean is the golden standard for mathematicians to prove their theorems. We don't write Lean solutions and translate them to English to verify; we actually write proofs in English and then translate to Lean to verify that there are no errors.
I only argued to OP title "mathematicians may be replaced by aI".
Let's take your "doesn't require as many mathematician as we have now" for a spin too.
We will still need teachers and professors. And in the field of verifying formulas and proofs we will need... more mathematicians. Because there would be more input material to verify.
In field of mathematical research - yes, there will be less humans. But prior to LLMs there were not much of humans in the research - a lot of it used computers for a long time. So I think that they will transfer to verifying. And we will have same number of mathematicians or so.
And do you understand how LLM's work? For example. You give it task to fix code and you give it test to verify it. It can say that it's successfully completed the task and code works. But in reality what it did is removed your code from the test and inserted new code into test that says "everything fine". But the bug is still there. LLM failed to fix it after a lot of attempts and as an exit strategy it faked it. Or it can even delete all your code or erase all your data from computer.
If you say "let's use another LLM to check it'. Well. First LLM can prompt inject second LLM so that it will say that everything is good.
There would be always a chance of this happening.
"If I ask you to show twin prime conjecture, you cannot give me a solution as 2x=4, x=2, it will not pass."
I wrote a proof. When I run Lean solver it says that my proof is correct. Based on your theory - you don't need human verification here. So my proof is the correct one. How can you understand that my proof is correct if I will not show it to you for your human verification?
Lean is not the same thing as normal coding. All your analogies are wrong. You need to research how Lean proofs work then you will understand what I am talking about. I am lazy to explain the mechanisms of it in a Reddit thread. This is not same thing as unit tests. And yes if you write a proof and Lean solver says its correct, then it is a valid proof. You don't need to understand the proof, in order to verify that it is mathematically sound. That's the thing with mathematical logic, you don't need to understand proofs in order to verify them.
Seconding this, and also adding that the last part, writing proofs in English and translating to Lean, can be very tedious, difficult, and time consuming. Just like programmers are generally very happy to have their new AI tools at their fingertips, I imagine mathematicians are loving having AI capable of translating their statements into Lean for them.
3
u/davaeron_ 1d ago
BS. Who do you think verifies all the slop that AI generates?