Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

Re:Titans of Mathematics Clash Over Epic Proof of ABC Conjec... by nabla9 on Thursday September 20, 2018 @05:20PM (#18035565)

Formal proof assistants and interactive theorem prover for mathematics already exist. So do proof libraries. See: http://metamath.org/

They are not used because it's tedious to type and proof every step in the process. Mathematicians don't write all steps down. You also need build a library from ground up.

We could to the same for computer programs but we don't wan to do that either.

[ Parent | on HN ]

Re:Titans of Mathematics Clash Over Epic Proof of ABC Conjec... by kiriakasis on Friday September 21, 2018 @03:38AM (#18037876)

Also I want to add syntax, mathematical syntax is incredibly rich, complex, ambiguous and effective; so much that in some paper it is the hardest part to understand, not always because of bad writing.

At least we are better off than theoretical physicists :-)

[ Parent | on HN ]