Deliverable 7

Tools for managing the dependencies between proofs, and querying and searching the database.

Tools for managing dependencies between proofs:

• DAMF: Distributed Assertion Management Framework

Tools for indexing definitions and theorems:

• Lambdapi >= 2.4.0 includes commands for indexing Dedukti and Lambdapi files, making complex search queries and running a web server for making queries on the web

Tools for searching libraries:

• Online Lambdapi Search Engine
• LeanExplore
• Loogle
• Moogle
• LeanSearch
• LeanCopilot
• Lean State Search
• Lean Finder
• FindFacts: search application to find formal theory content of Isabelle and the AFP
• SErAPIS: search engine for the Isabelle 2021 and Archive of Formal Proofs 2021 libraries