3 ms·
Open conjectures are usually solved by inventing new mathematical frameworks that embed the context of the existing question. Inventing new definitions is triv
by auntienomen 3y ago
Open conjectures are usually solved by inventing new mathematical frameworks that embed the context of the existing question. Inventing new definitions is trivial, but there's no rules that constrain the space of moves. And inventing _interesting_ new definitions is extremely hard. I wouldn't bet on LLMs doing this ever.
- auntienomen 3y agoWhat would be nice is an LLM to aid in translation between mathematics and a theorem proving language like Lean. That might fuel a revolution in how mathematics is done.