Explore our questions

1 vote
1 answer
40 views

What is the official way to reinstall Lean4 from scratch on a Mac or Linux?

0 votes
1 answer
61 views

How does one create a lean project and have mathlib import work when not creating the lean project at the $HOME directory?

0 votes
0 answers
18 views

How does one create a lean project even if it already exists e.g., lake +leanprover/lean4:nightly-2023-02-04 new my_project math?

6 votes
2 answers
235 views

Lean and inaccessible cardinals

3 votes
1 answer
219 views

Determining why my proof depends on the axiom of choice

2 votes
2 answers
164 views

How do I prove $\operatorname{succ}(a)$ cannot be equal to $0$ in Lean4?

15 votes
1 answer
732 views

Lean "nonempty" vs "inhabited"

0 votes
1 answer
69 views

What am I doing wrong when proving the add_right_cancel theorem?

1 vote
1 answer
98 views

Need help with induction proof in Lean for $0+d=d$

3 votes
1 answer
97 views

Implementing and verifying algorithms for solving equations in Lean

3 votes
4 answers
1k views

In Lean, why is it possible to prove $\text{succ}\; x \neq 0$ without adding it as an axiom?

1 vote
2 answers
162 views

Coq / Lean endpoint for GPT actions

1 vote
1 answer
94 views

How to see the value under Exists in Lean?

2 votes
1 answer
158 views

Verifying a basic function with Lean4

Browse more Questions