4 ms·
especially compared to existing 129 pages proof by human
by andriy_koval 1mo ago
especially compared to existing 129 pages proof by human
- dist-epoch 1mo agoInsert meme with 200 pages needed to prove 1+1=2 rigurously
- deleted 1mo ago[deleted]
- black_knight 1mo agoA human can cite previous published results. I am sure a lot of this development was formalising the prerequisites.
- andriy_koval 1mo ago> I am sure a lot of this development was formalising the prerequisites How can you be so sure its not result of inefficiency?
- black_knight 1mo agoOh, I am quite sure there are inefficiencies! Just that they are not entirely inefficiencies. I have used Fable for formalisation and it will, unless I catch it, reprove results it previously had proven, inline, in other results.
- itishappy 1mo agoA published formalization is code. I would not think humans have any edge when it comes to citing previously published results.
- Jaxan 1mo agoWouldn’t a lot already be in leans mathlib?
- throw567643u8 1mo agoAI is hopeless at using existing code, it likes to append only.