Titans of Mathematics Clash Over Epic Proof of ABC Conjecture

Re:Titans of Mathematics Clash Over Epic Proof of ABC Conjec... by davemp on Thursday September 20, 2018 @07:23PM (#18036154)

How current proof assistants work is using the Curry-Howard correspondence, [1] the gist of it is that all of first order logic can be encoded into a type. All one must do is write an expression that type checks to what one is trying to prove. That turns out to be fairly hard for reasonably complex proofs.

[1]: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

[ Parent | on HN ]

Re:Titans of Mathematics Clash Over Epic Proof of ABC Conjec... by Twisol on Thursday September 20, 2018 @09:27PM (#18036586)

To be only a little more precise, every proposition becomes a type of its own. The AND operator forms product types, the OR operator forms sum types, IMPLIES forms a function type... The proof of a theorem turns into an inhabitant of the theorem's type.

[ Parent | on HN ]