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. -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/fricas-devel/093f1dea-f690-4f03-9d7e-d39cb55cce79n%40googlegroups.com.
