Unanswered Questions
237 questions with no upvoted or accepted answers
27
votes
0
answers
805
views
Categorical semantics of Agda
I would like to know the state of the art regarding the categorical semantics of the type theory implemented by Agda — or at least some approximation of that type theory that is amenable to ...
- 3,480
16
votes
0
answers
274
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 ...
- 1,198
15
votes
0
answers
1k
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 ...
- 1,215
13
votes
0
answers
483
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-...
12
votes
0
answers
240
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 ...
- 3,480
12
votes
0
answers
219
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 ...
- 2,876
11
votes
0
answers
221
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 ,...
- 2,876
11
votes
0
answers
356
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 ...
- 1,215
10
votes
0
answers
643
views
Does CICω prove Con(ZF)?
Given that most major proof assistants are based on type theory (Coq, Lean, Agda), while the orthodox dogma is that all mathematics is based on set theory, it is very natural to ask how set theory and ...
- 1,815
10
votes
0
answers
222
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 ...
- 4,832
9
votes
0
answers
173
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 ...
- 383
8
votes
0
answers
259
views
What's the current state of the initiality conjecture for MLTT (and friends)?
By initiality conjecture (IC), I mean the following statement (nlab):
The term model of a type theory should be an initial object in the category of models of that type theory.
The emphasis is mine; ...
- 315
8
votes
1
answer
488
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 ...
CommunityBot
- 1
8
votes
0
answers
202
views
How to improve/understand typechecking performance in Agda?
I've recently been trying to do some basic formalization of category theory in Agda. As part of this I need to prove a bunch of basic properties around products/monoidal categories. A bunch of these ...
- 201
8
votes
0
answers
267
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 ...
- 81