This website is asking me for permissions on my phone. Why?
ngruhn 2 hours ago [-]
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.
corysama 2 hours ago [-]
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...
benlivengood 2 hours ago [-]
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.
ngruhn 2 hours ago [-]
Not saying this is useless. But that article reads like they made some kind of breakthrough in automatic software verification. But is sounds like they rather ported a tutorial test suite from Go to Rust with AI and the tests are still passing.
2 hours ago [-]
Rendered at 20:20:53 GMT+0000 (Coordinated Universal Time) with Vercel.
> 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...