Unanswered Questions

49 questions with no upvoted or accepted answers
19 votes
0 answers
187 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 ...
18 votes
0 answers
209 views

Can we automatically get around set-theoretic difficulties?

One of the main technical annoyances of working with (large) categories is the variety of set-theoretic difficulties that come about with it: if we use ZFC as background logic, then those large ...
16 votes
0 answers
133 views

Programming language metatheory in Lean 4?

I'm looking for developments of programming language metatheory done in Lean 4. We have a calculus with a lot of mutually recursive judgements and we want to formalise its denotational semantics. ...
16 votes
0 answers
116 views

Code generation from Locales and Sublocales in Isabelle

Problem Description I stumbled on this limitation/misunderstanding several times when using locales and sublocales in Isabelle. As a minimal example, let us extend the locale from the example in ...
12 votes
0 answers
279 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 ...
12 votes
0 answers
124 views

Rules for mutual inductive/coinductive types

Some proof assistants, like Agda and maybe Coq, allow families of mutually defined types, or nested definitions of types, in which some are inductive and others are coinductive. I have no idea what ...
11 votes
0 answers
182 views

Do any automated theorem provers have the ability to stop, save state, reboot computer, restore state, continue?

With automated theorem provers knowing ahead of time how long the search will take or even if it will find a solution is unknown. Often for long running searches one eventually just has to halt the ...
10 votes
0 answers
178 views

Unintentionally proven false theorem with type-in-type outside logic and foundations?

We are all familiar with Russell's paradox, and it is known that Per Martin-Löf proved that type-in-type is normalizing and consistent (which is false), by accidentally using an assumption in his meta-...
10 votes
0 answers
164 views

Is there a proof assistant (or an embedding) for the (co)end calculus?

A Higher-Order Calculus for Categories describes a system where you can conveniently perform manipulations with categories, functors, Yoneda embeddings etc. An example of the rules is: $$\frac{\Gamma ,...
10 votes
0 answers
304 views

What's "Swedish" style of doing type theory or proof assistants?

Jon Sterling said Conor McBride's universe polymorphism proposal to be: seems to have worked well in Swedish experiments I wonder, what does "Swedish" mean here? What kind of type theory ...
10 votes
0 answers
137 views

What are the practical differences between intensional and extensional type theories?

It is already proved that MLTT with equality reflection is equivalent to MLTT with an intensional equality, plus UIP and function extensionality. So theoretically the differences between intensional ...
8 votes
0 answers
68 views

Graph algorithms in Coq

We’re looking for a good library for reasoning about graphs in Coq. Some key features with would want to support include: Topological sorting (ideally along with other graph algorithms) Manipulation ...
8 votes
0 answers
79 views

What is focusing and how do I use it?

I have heard the term "focusing" with respect to the sequent calculus (System LK) and related calculi like the $\bar{\lambda} \mu \tilde{\mu}$-calculus. What is focusing and how do I use it? ...
8 votes
0 answers
101 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 ...
7 votes
0 answers
177 views

Alternatives to universe levels

All of the type theory based proof assistants that I have seen have an infinite hierarchy of type universes to avoid the type of types being a term of itself. Are there alternative systems which could ...

15 30 50 per page