3 ms·
Probably not since LLMs can now carry out very large formalizations (https://www.anthropic.com/research/formalizing-fermats-last-theorem https://www.anthropic.c
by minkowski 12d ago
Probably not since LLMs can now carry out very large formalizations (https://www.anthropic.com/research/formalizing-fermats-last-theorem https://www.anthropic.com/research/formalizing-fermats-last-...).
- rbanffy 10d agoUnless humans understand them, can we trust such formalisations? We can prove the formalisation is correct, but we can't prove it accurately reflects what we are trying to prove.