Dependency Visualization & Multi-Checker Verification for Lean 4
Welcome! Explore interactive examples of LeanDepViz in action. All demos run entirely in your browser - no server required.
These demos showcase dependency graphs, verification results from multiple tools, and the power of defense-in-depth verification.
Complete demonstration of defense-in-depth verification with three independent checkers analyzing test cases from LeanParanoia's test suite.
This demo uses manually crafted verification results to illustrate UI capabilities. SafeVerify results are mock data (requires two versions to compare, but test files exist in only one version).
Demonstrates SafeVerify's ability to detect when theorem statements change between reference and modified versions, even when both compile successfully.
This demo uses realistic mock data. See examples/safeverify-demo/ for reference and modified source files to run with real SafeVerify comparison.
Probability theory formalization with ~800 declarations. Demonstrates large-scale dependency visualization.
Strong Prime Number Theorem formalization with 1129 declarations from complex analysis and number theory.
All examples from LeanParanoia's test suite showing various exploits and verification scenarios.
This demo uses manually crafted verification results based on known issues in the LeanParanoia test files.
Minimal example with three declarations showing good and bad theorems. Good starting point.
Upload your own dependency graphs and verification reports. All processing happens in your browser - no data sent to servers.