9 ms·
The entire point of writing proofs is for advancing human understanding. A giant dump of symbols that passes the lean compiler is meaningless besides human bein
by fsmv 1mo ago
The entire point of writing proofs is for advancing human understanding. A giant dump of symbols that passes the lean compiler is meaningless besides human beings understanding it.
- variadix 1mo agoIn the field of pure mathematics this might be true, but it has implications regardless for applied math, engineering, and physics.
- esafak 1mo agoIs it the AI's fault we can't understand? If the GUT is beyond human comprehension does it matter less? We don't apply this reasoning to other animals or even to less capable humans. Besides, the robots may want to ponder maths for their pleasure.
- Jtarii 1mo agoAn AI may still be able to apply the results without humans understanding the proof.
- pfdietz 1mo ago> The entire point of writing proofs is for advancing human understanding. Proofs also enable AIs to direct search and generate knowledge. Verifiability is immensely useful for keeping AI grounded. One might imagine AI generating enormous numbers of hypotheses and then trying to prove or disprove them, and then mine that data for new abstractions and heuristics.
- fsmv 1mo agoBut what does it mean? The theorems are just symbols in lean. The conjectures humans chose are carefully selected to be the questions that are interesting and relevant to our intuition about the real world. Math often doesn't have applications for hundreds of years and that application is only possible because people deeply understand it and how it applies to the real world. Generating an endless list of true statements doesn't really do anything, those things are already true regardless of whether someone has written a lean program to model them.
- pfdietz 1mo agoLean terms and programs have defined meanings, just like anything mathematical does. It sounds like you're asking something nebulous, like does it have a soul. Mass generation of conjectures and proofs/disproofs could AI to discover objectively mathematically useful things. For example, it might discover shortcuts, lemmas, even abstractions that are useful in the proofs of these things -- and judge that utility by how much they improve the ability of the AI to prove things in this mass of problems. It wouldn't say whether the things are useful for non-mathematical human problems, but then human mathematicians, as you say, can't really judge that either.
- nullc 1mo agoSometimes the purpose of the proof is simply to demonstrate that some construct is a safe assumption for other more interesting work-- and could still serve that purpose even if it was entirely a black box.
- nickysielicki 1mo agowas. Not is. Was.
- dyauspitr 1mo agoNo it isn’t, it’s putting it into the corpus which means another LLM doesn’t have to spend a few billion credits the next time.