Viewing profile — kevinzz

Lean 4 is no longer being developed in private; this was true a year ago but is no longer true. What is true is that Lean 4 is still not ready for the port of the maths library to …

There is every way of knowing how much will be obsolete in Lean 4, as long as you're following the discussions at https://leanprover.zulipchat.com . The type theory of Lean 4 will …

The headline is clickbait. A more measured debate about the issues is here https://xenaproject.wordpress.com/2019/09/27/does-anyone-kno...

https://xenaproject.wordpress.com/2019/09/27/does-anyone-kno...

In Lean you could do theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p := by cc for a tactic proof and theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p := λ ⟨h,j⟩,⟨j,h⟩ for …