Finding bugs and inconsistencies in the Julia language: a really cool use of theorem proving based on Lean, and AI agents to do the dirty "handwork" that would otherwise be very very tedious. The source code of Julia itself is modeled in Lean and then is checked against what the code is *supposed* to be doing (based on documentation strings, manuals or obvious other properties).By Miles Cranmer, of the University of Cambridge.https://github.com/MilesCranmer/julia-in-lean#julia #ai #lean
Finding bugs and inconsistencies in the Julia language: a really cool use of theorem proving based on Lean, and AI agent...
