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

1 vote
2 answers
80 views

How to introduce assumption in lean4

7 votes
3 answers
272 views

Preserve equality with match expression

0 votes
1 answer
65 views

How to run lean4 with mathlib manually

2 votes
1 answer
97 views

How to Prove Theorem le_zero in Lean4: If x ≤ 0, then x = 0?

2 votes
1 answer
138 views

How to understand the sigma types example from "Theorem Proving in Lean 4"?

21 votes
3 answers
418 views

Programming language metatheory in Lean 4?

1 vote
1 answer
135 views

how to prove 2+2+a=4+a in lean4?

5 votes
2 answers
302 views

Type Theory Lean 3 to Lean 4

1 vote
1 answer
100 views

How to handle data from json files in lean 4?

2 votes
2 answers
92 views

Simplifying Array Access

6 votes
1 answer
288 views

Benefits of HoTT compared with dependent type theory like what Lean does?

2 votes
0 answers
99 views

Highschool level linear algebra

3 votes
1 answer
160 views

Understanding noConfusion

4 votes
1 answer
191 views

Programming challenge site for lean4

Browse more Questions