Skip to main content

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.

Filter by
Sorted by
Tagged with
1 vote
2 answers
129 views

Topic for undergraduate thesis

I'm an undergraduate student in my final year studying applied mathematics. To graduate, I need to present a thesis, and I'm considering using Lean and first-order predicate logic for my thesis. My ...
Hackerman's user avatar
  • 111
1 vote
0 answers
62 views

How to choose an axiom system in Isabelle/HOL?

First of all, sorry if my question is too nonsensical and naive, I'm just getting started with Isabelle/HOL. I am reading Hou's "Fundamentals of Logic and Computation: With Practical Automated ...
Red Banana's user avatar
1 vote
1 answer
56 views

Using coIH as an argument to the transitivity of Bisimilarity (cofix and pcofix)

It might be a very silly question for the logic gurus but less so for me. First I generally describe the issue, than I provide a proper example with code. Assume three streams of nats: xs, ys, zs. ...
Uladzimir Treihis's user avatar
4 votes
2 answers
185 views

Which proof assistants implement Church's rule?

Church's rule (CR) is one of the hallmarks of constructive mathematics, and is an admissible rule in a wide variety of constructive theories (you might consider CR to be a requirement for constructive ...
Christopher King's user avatar
4 votes
0 answers
120 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 ...
user23220385's user avatar
0 votes
0 answers
67 views

Research methodology in formal verification

Is there a written account on how to carry out research in formal verification with proof assistants? Formalisation of standard mathematics, verification of information systems and developing proof ...
Gergely's user avatar
  • 311
4 votes
1 answer
169 views

What is the best way to learn Iris completely independently

I am looking forward to learning Iris by myself, I have essential basic knowledge of Coq and logic but I don't know where to start. Logically, I looked into materials on the project website; the video ...
asha soroushpoor's user avatar
7 votes
1 answer
551 views

Examples of theories where tactic language is required for simple proofs

I was always under the impression, that separate tactic languages were generally considered to be vital for writing long proofs. I see tactic languages as a kind of interpreted DSL to generate ...
uhbif19's user avatar
  • 177
1 vote
2 answers
127 views

Is the Archive of Formal Proofs indexed in journal databases?

I was wondering if journals that publish regularly formal proofs are indexed in journal databases like Scopus or Web of Science. Apparently, this is not the case. Why is it so?
user1868607's user avatar
6 votes
1 answer
327 views

(Dis)Advantages of basing a proof assistant on CH correspondence?

Major proof assistants like Lean and Coq are fundamentally based on the Curry-Howard correspondence: propositions are encoded as types, quantified propositions are encoded as dependent types, proofs ...
Weier's user avatar
  • 313
2 votes
0 answers
104 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 ...
Gergely's user avatar
  • 311
2 votes
0 answers
81 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 ...
Julius Hamilton's user avatar
4 votes
1 answer
113 views

How do we know that we can trust proof assistance to produce correct results?

Well, pretty simple question, how do we know that we can trust the proof assistants? I ask this question as a complete lay in proof assistants. Maybe a trivial answer could be "because smart ...
Babu's user avatar
  • 269
7 votes
2 answers
1k views

Is it possible to make a proof assistant program based on ZFC?

I heard that many proof assistant programs are made based on the type theory. For me, as a mathematician, when I met Coq at first, it is difficult to accustomed with it. So I have a question. Is it ...
with-forest's user avatar
3 votes
2 answers
453 views

Are there minimal typed proof verifiers that can deal with the majority of mathematics?

I would like to know if there are proof verifiers that can deal with the majority of mathematics (definitions, theorems, proofs with verification), while also having a minimal implementation. I am not ...
Lewwwer's user avatar
  • 131
1 vote
0 answers
48 views

How do I prove this property about a factorial specification in Coq?

Notes: This post got pretty long... my apologies but hopefully somebody can take the time to look through it. Also, some of the code below uses terms that are defined elsewhere in my file and not ...
bodacious_bandit's user avatar
1 vote
1 answer
148 views

How do I prove an expression in Coq that involves pattern matching?

I'm working on a proof in Coq and my proof state is as follows: ...
bodacious_bandit's user avatar
3 votes
0 answers
45 views

How do proof assistants/ automated theorem provers compare with other symbollic tools like mathematica, maple or magma in terms of practicality [duplicate]

TLDR What are the advantages and disadvantages of using a proof assistant when compared to using tools like Mathematica in terms of practicality and usability/ease of use ? ChatGPT summary of the ...
userrandrand's user avatar
2 votes
2 answers
1k views

Make ChatGPT write formal proof from natural language proof

I know very little about proof assistants, but I played a little with Lean, so I have some basic knowledge of how they work. I was curious whether I could make ChatGPT convert some natural language ...
domotorp's user avatar
  • 131
6 votes
1 answer
493 views

Paths Between Quotient Types in Cubical Agda

I'm new to Cubical Agda and I am trying to define the dependent set eliminator for certain quotient types. In particular, my quotient type is the integers, quotiented by the absolute value function (<...
Max Fan's user avatar
  • 61
6 votes
1 answer
120 views

Is there any formalization (with any theorem prover) of the Bohm theorem for lambda-calculus?

I am an university student working on a thesis about λ-calculus. I'd like to know if there's any article or publication about proof assistant formalizations of the Bohm theorem ("any two normal ...
Gabriele Cecilia's user avatar
5 votes
3 answers
222 views

are there any standard proof formats?

I would like to know if there are any proof formats which is used to exchange proofs among proof assistants. I realize different proof assistants use different foundations but for those that have the ...
jude's user avatar
  • 53
7 votes
2 answers
2k views

Why are these two proofs so different?

I was messing around with toy lemmas in Idris and came up with this silly proof. ...
Nathan's user avatar
  • 358
3 votes
1 answer
122 views

Do implementations of a PA and of ATP have overlap?

I'm wondering how much overlap (read: code-reusage) there is between a PA and an ATP system. Are they based upon the same type system at least? I'm wondering, because right now I'm working on ...
HighAsAKiteOnMath's user avatar
10 votes
2 answers
2k views

How can we formalize a game where each player is a program having access to opponent's code?

How can we define in a proof assistant (eg., Coq) a notion of a 2-player game, where each player is a program that has access to the opponent's source code? Background: In Open Source Game Theory, we ...
Matthias Georg Mayer's user avatar
2 votes
1 answer
150 views

Does there exists a logical format so that my app can export in that format, and the existing popular proof assistants can take it as input?

I'm creating a "CAS for category theory / homological algebra" in C++ that "supports proofs". Although it is feature creep, I was wondering if there exists a format that my app ...
HighAsAKiteOnMath's user avatar
9 votes
2 answers
916 views

Learning Math Proof via Proof Assistants

I want to learn proof based mathematics and it looks like a proof assistant like Coq and Lean could be a good way to go about verifying my proofs, without needing a PhD on hand to check through all my ...
quidproquo's user avatar
3 votes
1 answer
135 views

Difference between implementation and formalisation in a proof assistant

Some authors refer to their works as "implementation of the theory in (let's say) Agda", some refer as "formalization of the theory in Agda". What is the difference between them?
phdstudent's user avatar
5 votes
1 answer
81 views

Semantics verification of an LTL fragment logic

I am a beginner to Isabelle and I went over the proof documentation. I am trying to implement a fragment logic of LTL over finite intervals and finite traces called MLTL, the syntax and semantics can ...
Gokul's user avatar
  • 53
9 votes
2 answers
441 views

Comparison between proof assistants for coinductive structures and proofs

I have a quite vague and naïve question: what are the differences between the different proof assistants regarding coinduction? My motivation is that I'd like to formalize some proofs, basically about ...
sparusaurata's user avatar
6 votes
1 answer
197 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,...
Rob's user avatar
  • 242
20 votes
0 answers
233 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 ...
Jason Gross's user avatar
  • 1,537
25 votes
2 answers
386 views

How to use a proof assistant to reason in a topos?

I would like to use a proof assistant to reason in the internal language of a topos. More specifically, I would like to (be able to) formalise informal arguments such as in Ingo Blechschmidt's PhD ...
Nico's user avatar
  • 722