'A-Team' of Math Proves a Critical Link Between Addition and Sets

Re:'A-Team' of Math Proves a Critical Link Between Addition ... by zozbot234 on Friday December 08, 2023 @07:10PM (#38576720)

If the foundations are workable (and they seems to be, though IIRC there is a quotienting construct that's quite ad hoc and that people have complained about), the fact that you can additionally "assume" other things is fairly irrelevant, these are no different than extra axioms.

[ Parent | on HN ]

Re:'A-Team' of Math Proves a Critical Link Between Addition ... by staunton on Sunday December 10, 2023 @02:42PM (#38594279)

It's not useful to prove that "your program does what you want, provided the following 10000 functions implemented in C do what we assumed they do". Almost certainly at least one of them doesn't.

There isn't even a straightforward (let alone verified) way to list all assumptions of this type for some proof (you can print the axioms that a definition depends on, but that's not the same thing). It's possible to prove `false` in Lean using functions you'd normally use to make pretty much any useful program.

[ Parent | on HN ]