Unanswered Questions
30 questions with no upvoted or accepted answers
20
votes
0
answers
243
views
What is known about performance bottlenecks in proof assistants?
Background
In my personal experience, the biggest bottleneck to broader adoption of proof assistants (in industry and mathematics) is the effort it takes to engineer proofs. (In lines of code, for ...
- 1,132
6
votes
1
answer
209
views
Tools to formally verify programs written in languages supported by the GNU Compiler (GCC)
Is there a website that maintains a list, or is there a list, of tools that support verification of programs written in languages supported by the GCC compiler front ends: C, C++, Objective-C, Fortran,...
- 436
4
votes
0
answers
142
views
How do I write a definition/theorem with an arbitrary number $n$ of types?
I am trying to use mathlib to write the definition of a monoidally well-pointed monoidal category. This definition goes like: For all parallel pairs of morphisms $f, g : A_1 \otimes \cdots \otimes A_n ...
- 41
4
votes
0
answers
125
views
Proving "proof methods" as theorems in type-theory based proof systems
For example, suppose we have proved associativity of some binary operator $+ : T \to T$ as
add_assoc : forall (x y : T), x + y + z = x + (y + z).
We can thus prove ...
- 41
4
votes
0
answers
365
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?
- 141
4
votes
0
answers
363
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 ...
- 171
4
votes
0
answers
168
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 ...
- 41
3
votes
0
answers
70
views
Manipulating Summations ∑ and telescopic sums in Lean 4
I want to prove the following lemma:
...
3
votes
0
answers
195
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 ...
- 243
2
votes
0
answers
161
views
Defining Brownian Motion in Lean4
(Disclaimer: I'm worried that this question will appear lazy, but I did spend some time on it and am about to give up.)
In Mathlib, under probability, there are processes, filtrations and martingales. ...
- 101
2
votes
0
answers
101
views
Proof Checking for State Machines Similar to TLA+
I'm wanting to find a modern proof assistant that I can use for modeling distributed systems or similar protocols/algorithms.
TLA+ is the most commonly used language in that field, but I recently ...
- 11k
2
votes
0
answers
111
views
Algebraic manipulation: what is the best tool?
I have a set of algebraic axioms. I need to prove an equation, an algebraic law. What I did was applying "trivial" rewrite rules by a theorem prover from both ends, and then an automatic ...
- 323
2
votes
0
answers
85
views
Formally verified email or communication?
This question is contextualized by having an account hacked which is prompting me to move towards something I’ve long wanted to anyway.
I would like to consider the simplest possible formally verified ...
2
votes
0
answers
114
views
Must-read Lean 4 Mathlib Files
I am starting to understand Lean 4, but I feel a bit overwhelmed by the amount of dependencies for most files in Mathlib. To become more familiar, particularly with the module typeclass, I decided to ...
- 516
1
vote
0
answers
29
views
In Lean 4 prover, how to include a constructor into the search scope of a tactic?
I'm translating a soundness proof of system F- from Rocq to Lean 4.
Here is part of the relevant Rocq code:
...
- 131