News for hackers. Stuff that matters.

A comment on Mathematicians welcome computer-assisted proof in ‘grand unification’ theory. Parent comment

Re:Mathematicians welcome computer-assisted proof in ‘grand ... by chriswarbo on Saturday June 19, 2021 @08:24PM (#27565856)
I haven't used quotients (or Lean), but I've certainly encountered subject reduction problems in Coq when using coinduction, so this sounds a tad hypocritical.

It's certainly good to avoid breaking subject reduction even more though ;)

[ Parent | on HN ]
Re:Mathematicians welcome computer-assisted proof in ‘grand ... by Jweb_Guru on Saturday June 19, 2021 @10:38PM (#27566628)
Pierre Pedrot has been very vocal in his belief that broken SR from coinductive types is a serious problem with Coq that needs to be fixed. This is quite different from introducing stuff that deliberately breaks it.
[ Parent | on HN ]
Re:Mathematicians welcome computer-assisted proof in ‘grand ... by xvilka on Saturday June 19, 2021 @10:25PM (#27566547)
There's ongoing work[1] on fixing that. Also let's see how migrating setoids to cubical type theory might fix more issues for Coq. Will they follow the Arend[2] path? That remains to be seen.

[1] https://github.com/coq/coq/pull/10764

[2] https://arend-lang.github.io/about/arend-features

[ Parent | on HN ]