As far as I remember, The proof of Perelman of the Geometerization Conjecture took a year to check by the experts.
The claimed proof of the ABC conjecture Mochizuki took few years to check, and Peter Scholze another great mathematician rejected the proof while Mochizuki who is also another respected mathematician still insists the proof is correct as far as I am aware.
The classification theorem of finite simple groups is also another example where the proof is so long that very few people can actually understand it and so the rest of the community has to be skeptical.
My Position: If a proof is written in a formal language and checked on an automated proof checker, then for all practical purposes there is no reason to be skeptical anymore.
The problem is that human mathematicians do not write proofs in a formal language because it is a very exhausting process (possibly infeasible with the long proofs like that of Perelman or Mochizuki). Instead mathematicians write argument that mixes between mathematical formal language and human natural language in an effort to convince the reader that theoretically this argument could be turned into a formal proof.
Question: Given the success of ChatGpt in dealing with human natural language, did anyone attempt to use a variant of ChatGpt that would take as input a human written mathematics published paper and then output a formal proof which could then be checked by an automated proof checker ?
(1) "Given the success of ChatGpt in dealing with human natural language" ??
Maybe Chatgpt can itself answer this question , no humans needed here !!
(2) Currently , Chatgpt is a little toy with no understanding of logic & mathematics.
What output it gives is not mathematically valid beyond what inputs it was given earlier.
(3) There are Automated Theorem Proving Systems , which more suitable for such tasks.
Deterministic Processes & Mathematics & logic are involved there , unlike the Arbitrary & Probabilistic Processes in GenAI.
(4) Proof Verification is a somewhat easier task having some good Success.
In general , Proof Assistants can assist ( not replace ) Mathematicians.
UPDATES :
(5) OP "Are there attempts to use machine learning to settle disputes over long mathematical proofs?" : we can not use machine learning to settle disputes over short Proofs. Even less so for long Proofs , until & unless Humans check the Output Proof.
Why so ?
Say we have Proofgpt which converts human Proof P1 to formal Proof P2. Say Automatic Theorem Prover or Proof Assistant says P2 is indeed true. Who knows whether P1==P2 logically & mathematically ?
Human effort to check that will be more than original effort !!
Proofgpt is using Arbitrary & Probabilistic Processes to guess the intended meanings to then throw out some Proof , without really know what it means. There is no way to guarantee Equivalence.
When that output is long , humans can not check it.
Just like GenAI uses Probability & Belief Networks , we can only conclude that P2 is Probably same as P1 , with certain level of Belief.
(6) OP "I am asking for a machine that will do the boring task of translating a human proof to a formal proof" : Even if the machine converts it , humans have to check the conversion for logical soundness & mathematical validity. Eventually , there is no saving in effort.
It might make more effort.
references :
https://en.wikipedia.org/wiki/Proof_assistant
https://en.wikipedia.org/wiki/Automated_theorem_proving
https://www.theatlantic.com/technology/archive/2022/12/chatgpt-openai-artificial-intelligence-writing-ethics/672386/
https://www.livemint.com/technology/tech-news/only-2-4-in-math-is-chatgpt-turning-dumb-11689876696634.html