Skip to main content

Questions tagged [lean3]

Lean 3 is the previous version of the Lean theorem prover, and has an active "community" release. If using the final "official" release from 2019 (3.4.2) which is incompatible with [mathlib], make this clear in your question.

4 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
13 votes
0 answers

How to speed up Lean?

I've recently been writing my first somewhat serious proof in Lean. While doing that, I noticed that Lean gets slower very fast with increasing length of the proof (slower in the sense that whenever I ...
GraffL's user avatar
  • 471
2 votes
0 answers

Proving (((finset.range 50).erase 0).erase 1).sum id = (finset.range 50).sum id - 1

I'm trying to prove the statement (((finset.range 50).erase 0).erase 1).sum id = (finset.range 50).sum id - 1 in Lean 3. The mathlib theorem ...
Arnoud Nijon's user avatar
2 votes
0 answers

Proof of a certain proposition not using classical logic

I'm self-studying the textbook Theorem Proving in Lean, and there's one exercise from Section 3.7 that I'm stuck on. The exercise asks for a proof of the proposition ¬(p ↔ ¬p) that does not use ...
Gavin Dooley's user avatar
0 votes
0 answers

Porting Lean 3 to Lean 4 Process (and the state of general integration in Lean 4)

I found this reference for measure-theoretic integration in Lean. However, I cannot find any integration in the Lean 4 Measure Theory library. Have these not yet been ported, or can they be found ...
Alex Byard's user avatar