Re-imagining the Isabelle Archive of Formal Proofs

Since its inception in 2004 the Archive of Formal Proofs has grown in size but its interface and functionality have only been minimally improved. To transform the AFP into a more user-friendly and effective resource, we redesigned the website to meet modern web standards and practices. We ensure that our work is community-driven by basing the redesign on results from a survey of the Isabelle community. The site generation uses Hugo and is implemented as a proper Isabelle component, which also allows us to adapt the AFP metadata model to avoid inconsistencies in the future. Notable improvements include a responsive design, new theory browsing interface, integrated search, and enhanced navigation.