logoalt Hacker News

fsmvyesterday at 6:41 PM7 repliesview on HN

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.


Replies

variadixyesterday at 7:00 PM

In the field of pure mathematics this might be true, but it has implications regardless for applied math, engineering, and physics.

pfdietzyesterday at 7:23 PM

> 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.

show 1 reply
Jtariiyesterday at 7:04 PM

An AI may still be able to apply the results without humans understanding the proof.

nullcyesterday at 7:26 PM

Sometimes 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.

dyauspitryesterday at 8:31 PM

No 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.

esafakyesterday at 7:03 PM

Is 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.

nickysielickiyesterday at 8:07 PM

was. Not is. Was.