Questions tagged [proof-assistant]
A proof assistant, or interactive theorem prover, is a software tool to assist with the development of formal proofs by human-machine collaboration.
49 questions
0
votes
1
answer
148
views
Can formal reasoning really prove that any code is correct?
I’ve been thinking about this lately — we have all these formal verification tools, theorem provers, type systems, etc., and they do work for specific cases like compilers or microkernels.
But when it ...
- 1
5
votes
2
answers
686
views
What next book on Algorithmic Type-Checking do you recommend after reading Egbert Rijke's Intro to HoTT book?
Introduction to Homotopy Type Theory by Egbert Rijke is my current favorite book.
Since it teaches me about HoTT, but not necessarily about algorithmic type-checking, what resource do recommend after ...
2
votes
1
answer
85
views
Isabelle: cannot prove a have statement by using a lemma
I am trying to prove the have statement in the theorem below:
...
- 123
0
votes
0
answers
108
views
What would be a good next step for this Python proof assistant's development?
I have most of the backbone code in to make the following function compile, which is mostly expression-tree code.
I'm lost when it comes to actual proof engines though. What would be a good next step ...
2
votes
2
answers
187
views
I'm implementing somewhat of a proof assistant from scratch and would like to know how the goal splitting algo works in proof mode
So when you're operating Coq, Lean, or any other standard proof assistant, there's a concept of a proof goal: the proposition you'd like to arrive at given some assumptions. The user then applies ...
1
vote
1
answer
146
views
When is a programming language well-suited for a proof assistant?
This question can be seen as a follow-up to
Proof Assistants in OOP languages but more concrete:
I took a look at the Wikipedia article on proof assistants: https://en.wikipedia.org/wiki/...
1
vote
3
answers
124
views
Isolation and external access to the kernels of proof assistants
I currently have an idea and I'm wondering whether it could be implemented:
There is this system called Dedukti, which is essentially a kernel for various proof assistants. Can it be described that ...
2
votes
0
answers
72
views
How should this "naive proving tool / framework" work?
My background with implementing programming languages is zilch. Though I can write a parser using a parser generator, both in Python & in D. I understand a lot of homological algebra, and the ...
3
votes
1
answer
162
views
If you're implementing a proof assistant with a "Universe" OOP class that takes index, for $\mathcal{U}_i, i\geq 0$ should $i =$`int` or `bigint`?
I'm wondering how "deeply PA's explore the indexed universes". Does Lean allow any integer holdable in the memory of a computer bigint or have they ...
2
votes
2
answers
228
views
What it takes to formalize concrete models of ∞-categories in Lean 4, e.g. like rzk approach using 3-level type theory?
As I understand, then there are 2 approaches to the formalization of ∞-categories in the proof assistants. One approach is being made in Lean 4 and it is ∞-cosmoi https://emilyriehl.github.io/infinity-...
- 185
6
votes
3
answers
2k
views
Proof assistants for undergraduate analysis
I am looking for a program that would help me prove some elementary inequalities. What I mean by that is that:
I would tell the program some term written with usual functions, then I would tell him « ...
- 163
2
votes
1
answer
219
views
Searching for alternative of doing maths with pen and paper
I am curious about is there software alternative of doing math stuff instead of writing equations in pen and paper, I am in computer science and occasionally required to read proofs specially in ...
- 29
5
votes
2
answers
198
views
Formalization of constructive books
Has there been any attempt to formalize Bishop's "Foundations of Constructive Analysis" in any proof assistant? (Lean, Coq, Isabelle, ...)
Or "Foundations of Constructive Probability ...
- 81
2
votes
1
answer
325
views
Could proof assistants fill in single theorems automatically?
Would it be possible to only write declarations and conclusions and write a program that automatically fill in theorems used to derive those conclusions in LEAN 4? From my understanding, proof ...
- 194
3
votes
1
answer
290
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 ...
- 33