Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.

Sign up to join this community
Anybody can ask a question
Anybody can answer
The best answers are voted up and rise to the top

Explore our Questions

8 votes
2 answers
261 views

Strong induction on ℕ with function α → ℕ

5 votes
2 answers
152 views

How to prove in Lean that sums are distributive?

28 votes
1 answer
269 views

In Lean, what do double curly brackets mean?

2 votes
2 answers
437 views

Lean: dubious noncomputability

5 votes
1 answer
97 views

How do I convince the Lean 4 type checker that addition is commutative?

11 votes
3 answers
587 views

Calculus of (inductive) Constructions: Do inductive definitions increase proof strength?

6 votes
3 answers
130 views

Preserve equality with match expression

10 votes
1 answer
133 views

Explicit vs implicit universes in lean

14 votes
1 answer
458 views

What does the "motive is not type correct" error mean in Lean?

6 votes
1 answer
832 views

In Lean, contradiction tactic failed but actually goal accomplished

15 votes
1 answer
96 views

Extends vs including a typeclass argument

2 votes
1 answer
166 views

Lemma about splitting of homogeneous polynomial equations into irreducible equations

12 votes
1 answer
434 views

Lean "nonempty" vs "inhabited"

21 votes
1 answer
278 views

What is the difference between `leanprover` and `leanprover-community` GitHub repositories?

Browse more Questions