Lean

λ-calculus

Lean is like a universal translator

if prop A then prop B

A → B

f : ℝ → ℝ

f : ι → ℝ

an arrow between propositions to write a proposition

an arrow between types to define the type of a function

≥

=

arrows

category

tactics

linarith

by …

simp

by rw

sets

definitions

if we unroll the proof it’s just a chain of arrows

between prop A and prop B

theorem test : A → B :=
begin
  sorry
end

Curry howard corresponance