Questions tagged [lean]
Lean is a theorem prover and programming language, based on the calculus of constructions with inductive types. For version-specific questions, also add the [lean3] or [lean4] tags.
11
questions with no upvoted or accepted answers
13
votes
0
answers
424
views
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 ...
- 471
8
votes
0
answers
123
views
Has there been any work on automated translation of tactic proofs to everyday language?
There are times when I've completed a proof with a lot of backwards reasoning, and I've kind of lost the thread of what I've actually done. It would be nice if there was something that could ...
- 363
6
votes
0
answers
229
views
What would a fully classical and fully univalent ITP and library look like?
Consider two developments in dependent type theory:
Lean’s mathlib library (as well many other ITP libraries) is unashamedly fully classical. There is no ...
- 7,240
5
votes
0
answers
205
views
An algorithm for the substitution of formulas for predicates in first order logic
I am trying to find a detailed description of the definition of substitution of formulas for predicates in first order logic and an implementation of this as a function in Lean or Haskell. The aim is ...
- 419
4
votes
0
answers
234
views
Does Lean have a function that reads a file "at compile time"?
Is there some "pure" function that reads a file before the program is type-checked and returns its contents as a string or something, for example if the file ...
- 131
2
votes
0
answers
105
views
Highschool level linear algebra
I would like to be able to do high-school level linear algebra in Lean/Mathlib. However, it seems pretty hard. I do understand that mathematicians don't care about being able to do this basic stuff ...
- 173
2
votes
0
answers
135
views
Does Lean 4 have syntax to refer to the current thing being defined?
If I am defining a function (using def for example) then is there some way to refer to the function being defined inside its definition without using the name of ...
- 21
2
votes
0
answers
196
views
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 ...
- 121
1
vote
0
answers
117
views
Lean proofs for graph algorithms
I am new to lean but am interested in proving correctness of graph algorithms. Is there a repository/website that talks about a proof using lean of Dijkstra's shortest path algorithm, for example?
- 111
0
votes
0
answers
177
views
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 ...
- 456
-1
votes
0
answers
16
views
Lean predicate logic . Error in my proof , could anyone help?
This is a screenshot of the code. I have used exists elimination and or elimination to prove the statement above. However, it gives me an error and i'm not sure why.
- 1