Lawrence Paulson (Jun 01 2026 at 18:23): Lawrence Paulson (Jun 01 2026 at 18:23):Many thanks to Arthur Freitas Ramos for this great contribution!
"Announcing IsabelleBlueprint: a new project-layer tool for Isabelle/HOL formalizations. Inspired by Lean Blueprint but built specifically for Isabelle, it lets researchers describe a formalization plan in Markdown or LaTeX, turn it into a dependency graph, connect blueprint nodes to real Isabelle facts and AFP entries, track whether results are found, proved, tainted, or still planned, and publish progress through reports, badges, graphs, CI outputs, and a browsable HTML site. It also emits “ready” proof tasks with dependency context, making it easier for humans and AI agents to collaborate on large Isabelle developments.”
https://github.com/Arthur742Ramos/isa-blueprint
Last updated: Jun 12 2026 at 11:44 UTC