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 deadbeef57 on Saturday June 19, 2021 @03:35PM (#27563684)
In my experience, the difficulty is very rarely the transition from set theory to type theory. I find this almost transparent in practice.

The issue is rather that you need to deal with edge cases that are usually swept under the rug, or that you need to spend a full page working out the details of a proof that everyone recognizes as obvious. It would be great if computers could give even more assistance with these tedious parts of formalization, and I'm very glad that people are working hard on realizing this.

[ Parent | on HN ]
Re:Mathematicians welcome computer-assisted proof in ‘grand ... by chriswarbo on Saturday June 19, 2021 @08:15PM (#27565811)
One area I've been playing with is "theory exploration", which takes a set of definitions and produces lemmas that are 'interesting' (i.e. irreducible, via some scheme like Knuth-Bendix rewriting).

(Thanks to Curry-Howard, we can also view this as generating test suites/specifications for software libraries!)

Notable tools include Hipster, IsaScheme, IsaCoSy, QuickSpec and Speculate.

[ Parent | on HN ]
Re:Mathematicians welcome computer-assisted proof in ‘grand ... by ganzuul on Saturday June 19, 2021 @04:42PM (#27564290)
Kurt Gödel with a bat in dark alleyway of obviousness haunts my dreams.
[ Parent | on HN ]