Dan Piponi on Nostr: Formalised mathematics is, in a sense, a theory limited to *correct* mathematics. But ...

Formalised mathematics is, in a sense, a theory limited to *correct* mathematics. But when we're learning mathematics, and trying to derive new mathematics, we have to deal with vague, fuzzy, and incorrect mathematics all the time. I think that one failure of old school AI was that if you're, for example, exploring a space of well formed propositions derived from axioms, it's hard to pass through the space of half-baked ideas that humans use all the time as stepping stones.

I wonder if suitably harnessed LLMs could score in this area and that the almost human mistakes they make could ultimately turn out to be an advantage. The shortest path from concept A to concept B doesn't necessarily always pass through rigorous mathematics.