New math book rescues landmark topology proof

Re:New math book rescues landmark topology proof by webmaven on Thursday September 09, 2021 @02:46PM (#28473144)

> A good proof convinces someone that it's true; convincing a computer that it's true is probably tangentially useful, but not very interesting to most mathematicians. They mostly want to be expanding the frontiers of mathematical knowledge, not painstakingly encoding proofs that they already believe into a computer system.

I guess the question is which of "convincing a human" or "convincing a computer" is considered the higher bar.

In any case, uncovering "what you believe that isn't so" is pretty important.

[ Parent | on HN ]

Re:New math book rescues landmark topology proof by roywiggins on Thursday September 09, 2021 @03:15PM (#28473507)

Right, but the ordinary methods of doing mathematics seem to be so good that the vast effort required to encode proofs well enough for a computer to check vastly dwarfs the benefit, at least for now.

There's obviously been a lot of work done on proof assistants and maybe it will become easy and natural to formulate most proofs in a way a computer can check, but it's not anywhere close to that yet. The book explicating the proof discussed in the article is already 500 pages long, translating that into something a computer could check just isn't at all feasible yet.

[ Parent | on HN ]