← Back to context Comment by andriy_koval 13 hours ago especially compared to existing 129 pages proof by human 8 comments andriy_koval Reply black_knight 11 hours ago A human can cite previous published results. I am sure a lot of this development was formalising the prerequisites. itishappy 9 hours ago A published formalization is code. I would not think humans have any edge when it comes to citing previously published results. Jaxan 3 hours ago Wouldn’t a lot already be in leans mathlib? throw567643u8 2 hours ago AI is hopeless at using existing code, it likes to append only. andriy_koval 11 hours ago > I am sure a lot of this development was formalising the prerequisitesHow can you be so sure its not result of inefficiency? black_knight 11 hours ago Oh, 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. dist-epoch 12 hours ago Insert meme with 200 pages needed to prove 1+1=2 rigurously
black_knight 11 hours ago A human can cite previous published results. I am sure a lot of this development was formalising the prerequisites. itishappy 9 hours ago A published formalization is code. I would not think humans have any edge when it comes to citing previously published results. Jaxan 3 hours ago Wouldn’t a lot already be in leans mathlib? throw567643u8 2 hours ago AI is hopeless at using existing code, it likes to append only. andriy_koval 11 hours ago > I am sure a lot of this development was formalising the prerequisitesHow can you be so sure its not result of inefficiency? black_knight 11 hours ago Oh, 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 9 hours ago A published formalization is code. I would not think humans have any edge when it comes to citing previously published results.
Jaxan 3 hours ago Wouldn’t a lot already be in leans mathlib? throw567643u8 2 hours ago AI is hopeless at using existing code, it likes to append only.
andriy_koval 11 hours ago > I am sure a lot of this development was formalising the prerequisitesHow can you be so sure its not result of inefficiency? black_knight 11 hours ago Oh, 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.
black_knight 11 hours ago Oh, 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.
A human can cite previous published results. I am sure a lot of this development was formalising the prerequisites.
A published formalization is code. I would not think humans have any edge when it comes to citing previously published results.
Wouldn’t a lot already be in leans mathlib?
AI is hopeless at using existing code, it likes to append only.
> I am sure a lot of this development was formalising the prerequisites
How can you be so sure its not result of inefficiency?
Oh, 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.
Insert meme with 200 pages needed to prove 1+1=2 rigurously