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
Filter by
Sorted by
Tagged with
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 ...
GraffL's user avatar
  • 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 ...
march's user avatar
  • 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 ...
Jason Rute's user avatar
  • 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 ...
user695931's user avatar
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 ...
mr snuggles's user avatar
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 ...
Adomas Baliuka's user avatar
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 ...
adrian's user avatar
  • 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 ...
Gavin Dooley's user avatar
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?
Simd's user avatar
  • 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 ...
Alex Byard's user avatar
-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.
sophie's user avatar
  • 1