Bridging proof and computation (For a verified Lean–Macaulay2 interface). ~ Matthew Ballard, Anton Leykin, Damiano Testa, Michael Stillman. https://www.renaissancephilanthropy.org/bridging-proof-and-computation-a-verified-leanmacaulay2-interface #AI #Math #ITP #LeanProver #CAS #Macaulay2
