Lean theorem prover

Lean theorem prover
[Google Scholar] [Website] [Wikipedia]

Notes: interactive theorem prover

Lean is an interactive theorem prover and programming language developed at Microsoft Research.

Dependent type

  • The Lean theorem prover (system description) [demoura:cade:2015]
  • Indexed streams: A formal intermediate representation for fused contraction programs [kovach:pldi:2023]