News for hackers. Stuff that matters.

A comment on Titans of Mathematics Clash Over Epic Proof of ABC Conjecture. Parent comment

Re:Titans of Mathematics Clash Over Epic Proof of ABC Conjec... by forkerenok on Friday September 21, 2018 @01:50AM (#18037433)
The bottleneck is not the tool itself, but the theory it builds upon: Calculus of Constructs in Coq's case. CoC and other calculi oriented towards proofs have limitations.

To better understand current challenges with provers I can recommend this episode of the Type Theory podcast with Dan Licata as a guest: http://typetheorypodcast.com/2015/01/episode-3-dan-licata-on...

It's quite dense, but there are some bits that I, as a programmer, could understand.

[ Parent | on HN ]
Re:Titans of Mathematics Clash Over Epic Proof of ABC Conjec... by Jweb_Guru on Friday September 21, 2018 @05:46AM (#18038427)
The vast majority of formal proofs don't run into any limitations with the CiC. They run into more practical limitations with the tooling and available libraries and tactics.
[ Parent | on HN ]