3 ms·

Thanks! I wonder if it would work better on proofs expressed in a formal proof-assistant language. Like, if we took something with GPT's training but also speci

Thanks! I wonder if it would work better on proofs expressed in a formal proof-assistant language. Like, if we took something with GPT's training but also specifically exposed it to large amounts of Lean/Agda/Coq/whatever, might it learn to construct proofs in the formal language better than it can in English/LaTeX?

graycat 3y ago
Commonly in high school, students learn to do proofs in a few days/weeks from a few dozen examples. Sorry, best I can guess, the basic technology of ChatGPT can't learn an equivalent way of doing proofs even from millions of proofs. It would be really interesting if the ChatGPT learning could learn proof writing, but my guess is that with ChatGPT too much is missing. Here is a point: Earth is awash in animals with brains that are built a lot like human brains, but I can't think of even one such animal that has a chance of keeping up with a standard course in plane geometry. Why? Something is missing, humans have it and only humans. Yes, your suggestion of adding structure to the data has a chance. Maybe with enough structure proof writing can reduce to looking for a path through a network, roughly what, say, a chess program has to do.