Is this impressive? They just ported a bunch of theorems/proofs already written in Rocq into Lean. Also Logical Foundations is just a Rocq tutorial with the basics. An absolutely amazing tutorial and probably the best resource out there. But I'm not surprised AI can do that.
I believe what they are bragging about is not the translated proofs, but the process of doing the translation.
> produced by frontier AI with ~2 person-days of human effort versus an estimated ~2.75 person-years manually (a 350x speed-up). We achieve this through task-level specification generators...
Impressive if for no other reason than there are various disparate formally verified projects (seL4, compcert, certikos) that could potentially be unified under a single proof system. Additionally it may be possible to quickly extend existing proofs (e.g. seL4's proofs) to other architectures.
Is this impressive? They just ported a bunch of theorems/proofs already written in Rocq into Lean. Also Logical Foundations is just a Rocq tutorial with the basics. An absolutely amazing tutorial and probably the best resource out there. But I'm not surprised AI can do that.
I believe what they are bragging about is not the translated proofs, but the process of doing the translation.
> produced by frontier AI with ~2 person-days of human effort versus an estimated ~2.75 person-years manually (a 350x speed-up). We achieve this through task-level specification generators...
Impressive if for no other reason than there are various disparate formally verified projects (seL4, compcert, certikos) that could potentially be unified under a single proof system. Additionally it may be possible to quickly extend existing proofs (e.g. seL4's proofs) to other architectures.