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