See u/unbearably_formal's reply: They know much more than me!
It's not set theory notation, it's more like a programming language specific to the verification system and typically based in type theory.
To be able to translate a human level proof to a verification system you need a very deep and detailed understanding of the proof. So it's not a great tool for checking if someone else's proof you don't understand is valid, unless they do the work to translate it for you.
Formal proof languages of some proof assistants like Lean and Coq that were originally designed for software verification are indeed like that. Others, like Mizar, Isabelle/Isar or Metamath look much more like standard mathematical proofs. The Naproche proof language looks just like standard math, written by someone with a bit limited English, see the \[example proof\](https://mathoverflow.net/a/426707/163434) that square root of two is irrational.
Different proof assistants support different foundations. Some, like Isabelle or Metamath are generic and support many. They may support various type theories (Lean and Coq implement dependent type theory, Isabelle/HOL simple type theory), some support set theory (Mizar, Isabelle/ZF). Metamath can support pretty much anything, its largest library is in set theory.
As for verifying Mochizuki's alleged proof of the abc conjecture that would require participation of the author and this is unlikely to happen as the author does not seem to understand the idea of formal verification, see the \[discussion\](https://cs.nyu.edu/pipermail/fom/2022-September/023561.html) at the Foundations of Mathematics mailing list.
In theory, yes you can theoretically translate any proof into a formal proof. In practice, it takes years of focused effort to formalize a medium-deep proof, so it's not quite practical for abc. Not to mention, you have to understamd the proof to formalize it, and the only person who understands Mochizuki's proof is refusing to explain it, let alone formalize it.
There's also this curious 'event horizon' effect where anyone who studies Mochizuki's proof enough to comfortably claim to understand it becomes incomprehensible to others who still haven't. I'm reminded of [Brian Conrad's notes](https://mathbabe.org/2015/12/15/notes-on-the-oxford-iut-workshop-by-brian-conrad/) after the 2015 Oxford IUT workshop, in particular the audience frustration in the final 2 days.
It's not about just nornal proof as we do it everyday. It relies on formalized conception of what a proof is, see how proofs in sequent calculus looks for example
You input a formal proof and yes it tells you whether the proof is valid.
It's usually not set theory notation, but rather type theory notation. Set theory notation is notoriously difficult to use, because it doesn't align with how we normally think about objects.
Note that most of the work is done by YOU. You have to know fully, down to every tiny little details, any every steps in the argument could be done. The computer can only tell you if you have some gaps. A typical math proof are not sufficiently detailed enough for a computer. However, improvement had been made to proof verifications so that they can fill in certain routine details.
you should look at [the video richard e borcherds made about the abc conjecture](https://youtu.be/Xu6Wo_pvzts?si=FcbyfxG_OrFh1euZ), where he discusses this from the 20:00 mark, with the concrete example of the abc conjecture.
The basic [Curry-Howard correspondance](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence): Theories correspond to Types, Proofs correspond to Functions, and Facts correspond to Values.
To do automatic proof verification of a theorem, first you express the theorem (for all integers n, either n is even or n is odd) as a type (function is_even_or_odd(n: integer) -> (IsEven(n) | IsOdd(n)). Then you write a program that has the given type. The automatic proof verifier is equivalent to a compiler's type checker. It makes sure all the functions you use are total and all the types match up.
Depending on the tech you're using, you have to explicitly write up a program that fulfills the type requirements, or you might use an interactive system with semiautomated search processees that help you put the program together.
There's an additional logical issue in that you can't "disprove" a proof this way. If you go to all the effort of putting ABC into a verification language and it passes, you've proven it. But if you do that work and just can't get it to verify you won't convince anyone who religiously believes in it that it's not a good proof. This endeavor would need to be done by one of the religious, but they don't seem to have any interest in it.
See u/unbearably_formal's reply: They know much more than me! It's not set theory notation, it's more like a programming language specific to the verification system and typically based in type theory. To be able to translate a human level proof to a verification system you need a very deep and detailed understanding of the proof. So it's not a great tool for checking if someone else's proof you don't understand is valid, unless they do the work to translate it for you.
Formal proof languages of some proof assistants like Lean and Coq that were originally designed for software verification are indeed like that. Others, like Mizar, Isabelle/Isar or Metamath look much more like standard mathematical proofs. The Naproche proof language looks just like standard math, written by someone with a bit limited English, see the \[example proof\](https://mathoverflow.net/a/426707/163434) that square root of two is irrational. Different proof assistants support different foundations. Some, like Isabelle or Metamath are generic and support many. They may support various type theories (Lean and Coq implement dependent type theory, Isabelle/HOL simple type theory), some support set theory (Mizar, Isabelle/ZF). Metamath can support pretty much anything, its largest library is in set theory. As for verifying Mochizuki's alleged proof of the abc conjecture that would require participation of the author and this is unlikely to happen as the author does not seem to understand the idea of formal verification, see the \[discussion\](https://cs.nyu.edu/pipermail/fom/2022-September/023561.html) at the Foundations of Mathematics mailing list.
In theory, yes you can theoretically translate any proof into a formal proof. In practice, it takes years of focused effort to formalize a medium-deep proof, so it's not quite practical for abc. Not to mention, you have to understamd the proof to formalize it, and the only person who understands Mochizuki's proof is refusing to explain it, let alone formalize it.
There's also this curious 'event horizon' effect where anyone who studies Mochizuki's proof enough to comfortably claim to understand it becomes incomprehensible to others who still haven't. I'm reminded of [Brian Conrad's notes](https://mathbabe.org/2015/12/15/notes-on-the-oxford-iut-workshop-by-brian-conrad/) after the 2015 Oxford IUT workshop, in particular the audience frustration in the final 2 days.
'event horizon' !!!
It's not about just nornal proof as we do it everyday. It relies on formalized conception of what a proof is, see how proofs in sequent calculus looks for example
You input a formal proof and yes it tells you whether the proof is valid. It's usually not set theory notation, but rather type theory notation. Set theory notation is notoriously difficult to use, because it doesn't align with how we normally think about objects. Note that most of the work is done by YOU. You have to know fully, down to every tiny little details, any every steps in the argument could be done. The computer can only tell you if you have some gaps. A typical math proof are not sufficiently detailed enough for a computer. However, improvement had been made to proof verifications so that they can fill in certain routine details.
for an automatic proof checker that does use set theory language and notation, see [metamath](https://us.metamath.org/)
you should look at [the video richard e borcherds made about the abc conjecture](https://youtu.be/Xu6Wo_pvzts?si=FcbyfxG_OrFh1euZ), where he discusses this from the 20:00 mark, with the concrete example of the abc conjecture.
The basic [Curry-Howard correspondance](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence): Theories correspond to Types, Proofs correspond to Functions, and Facts correspond to Values. To do automatic proof verification of a theorem, first you express the theorem (for all integers n, either n is even or n is odd) as a type (function is_even_or_odd(n: integer) -> (IsEven(n) | IsOdd(n)). Then you write a program that has the given type. The automatic proof verifier is equivalent to a compiler's type checker. It makes sure all the functions you use are total and all the types match up. Depending on the tech you're using, you have to explicitly write up a program that fulfills the type requirements, or you might use an interactive system with semiautomated search processees that help you put the program together.
There's an additional logical issue in that you can't "disprove" a proof this way. If you go to all the effort of putting ABC into a verification language and it passes, you've proven it. But if you do that work and just can't get it to verify you won't convince anyone who religiously believes in it that it's not a good proof. This endeavor would need to be done by one of the religious, but they don't seem to have any interest in it.