Jonathan Julian Huerta y Munive (Mar 05 2026 at 16:06): Jonathan Julian Huerta y Munive (Mar 05 2026 at 16:06):Hello, this week Josef Urban and I recreated his autoformalisation experiment in Isabelle. Surprisingly, the agent was able to finish the objective (prove Urysohn's lemma) without extra tooling (we only asked it to run isabelle build). I also wanted to experiment using the agents for producing software and the result are these CLI tools for exposing certain Isabelle commands to the terminal. This should make autoformalisation workflows easier for the agents. I welcome feedback about these results from all members of the community, and specially from expert Isabelle developers.
Last updated: Mar 11 2026 at 08:47 UTC