Skip to content
← Tags

Topic

lean4

1 site entry connected to this topic.

Hall

Hall entries that share this topic

View all →

The Iron Formalist Medal

For proving that a theorem prover can also be a serious programming language.

Math & Formalism

Lean 4

A functional programming language and interactive theorem prover where formal mathematics and real software share one toolchain.