Formal Land

Utensil's monorepo for formalization, e.g. Lean, Aya.

Included explorations

I explore with the following formalization systems, and do interactive literate programming when supported, because then one can interact with the formalization and inspect intermediate (goal) states just from a Web browser.

• Lean 4 explorations on
  • annotated by alectryon
  • Edge Lean 4
    • preferably follow the latest Lean 4 release candidate
  • Duper
    • likely to follow a latest Lean 4 stable release
  • Verso
    • likely to follow an older Lean 4 stable release
  • SciLean (nothing yet)
    • likely to follow an older Lean 4 unstable release
• Aya
  • haskeller-tutorial
  • prover-tutorial
  • literate
• TLA+
  • pluscal.pdf

In scope

• Coq (renaming to Rocq): an interactive theorem prover
  • particularly with math-from-nothing
• Agda
  • particularly with 1lab
• Isabelle
  • Simple type theory is not too simple: Grothendieck’s schemes without dependent types
  • Lie Groups and Algebras
  • Topological Groups
• Metamath, see also Metamath-knife (in Rust)
• Mizar, see also mizar-rs
• egg, see also egglog and lean-egg
• Charon: process Rust crates and convert them into files easy to handle by program verifiers
• Kani: a bit-precise model checker for Rust, particularly useful for verifying unsafe code blocks
• Aneris: a higher-order distributed concurrent separation logic for developing and verifying distributed systems, built on Iris and Coq
• Dafny: a verification-aware programming language that has native support for recording specifications and is equipped with a static program verifier, used by Cedar before porting to Lean 4
• F*: a general-purpose proof-oriented programming language, supporting both purely functional and effectful programming. It compiles to OCaml, and C.
• Z3: an efficient SMT (Satisfiability Modulo Theories) solver with specialized algorithms for solving background theories.

Related (mostly CAS)

• GAP - Groups, Algorithms, Programming: a System for Computational Discrete Algebra
• Macaulay2: a software system devoted to supporting research in algebraic geometry and commutative algebra
• Singular: a computer algebra system for polynomial computations, with special emphasis on commutative and non-commutative algebra, algebraic geometry, and singularity theory
• GiNaC: a C++ library for symbolic mathematical calculations
• FLINT: a C library for doing number theory, which incooperates Calcium that provides exact computation with real and complex numbers.