Coding and Debugging are "old school".

[Tim Daly]

Things have changed quite a bit since January.

This is one of several systems, such as Devin, that can write new code,

write test cases, find errors, create fixes, and generate a patch.

https://www.youtube.com/watch?v=9-JBHGlYEBI&ab_channel=MatthewBerman

I've been qualifying 71 LLMs to see if and how well they can prove the GCD theorem.

Almost all can. Once this effort completes it seems worthwhile to see if they can

correctly create the GCD algorithm in Lisp.

Combining this capability with LEAN's proofs-as-code implies the ability to

create provably correct algorithms automatically.