Stack Exchange
log in sign up chat discuss faq users badges

Area 51 » Science

definition commitment

This proposal has reached 100% commitment. We are preparing for its launch and expect to create it soon.

221
followers

Proof Assistants

Proposed Q&A site for mathematicians and computer scientists who develop and use proof assistants.
flag

This proposal is now in the Commitment phase — example questions are locked!

64 Example Questions

active newest votes
up vote 28 down vote
I am a long-time Coq user who is learning Lean. Is there a short translation table mapping Coq tactics to corresponding Lean tactics?
added by Andrej Bauer Nov 19 at 21:36
link|flag
up vote 19 down vote
Is there a way to automatically translate proofs from one proof assistant to another?
added by Kevin Buzzard Nov 19 at 23:52
link|flag
up vote 18 down vote
Why, after all these years, is append not obviously associative?
added by pigworker Nov 19 at 21:40
link|flag
3  
More of a comment than a question, amirite? – Cactus Nov 20 at 3:17
up vote 15 down vote
What is the difference between a datatype's parameters and indexes? Why do we have both concepts?
added by Potato44 Nov 20 at 4:34
link|flag
up vote 14 down vote
I want to use Lean to teach Algebra to my students. Has anyone done it? How did it go?
added by arthur Nov 19 at 23:28
link|flag
up vote 14 down vote
How do I implement a proof assistant and what are the essential papers I need to read to do it?
added by Anton Trunov Nov 20 at 11:23
link|flag
up vote 12 down vote
Is there a formalization of the fact that finite limits commute with filtered colimits?
added by Dan Christensen Nov 19 at 21:52
link|flag
You would probably want to state which proof assistant you have in mind. That can also be accomplished with a tag, but people may not notice it. – Andrej Bauer Nov 19 at 21:59
2  
I think in some cases one might be interested in a formalization in any proof assistant. That's true for this (real) question, so I didn't specify. – Dan Christensen Nov 19 at 22:25
Yes, I agree it need not be specific to a particular proof-assistant. – Andrej Bauer Nov 19 at 22:32
4  
(answer to real question is "yes in Lean: leanprover-community.github.io/mathlib_docs/…) – Kevin Buzzard Nov 19 at 23:54
up vote 12 down vote
What is a better way of doing this in Lean: `have H := ..., simp at H, apply H`? If I just do `apply ...` it fails to match against the goal.
added by Andrej Bauer Nov 19 at 22:25
link|flag
up vote 12 down vote
Why most assistants forbid recursive datatype occurrences in negative positions, i.e., in front of a ->?
added by Dokkat Nov 19 at 22:44
link|flag
up vote 12 down vote
What are the pros and cons of having impredicative universe Prop in theorem provers based on dependent type theory?
added by Anton Trunov Nov 20 at 8:06
link|flag
up vote 12 down vote
Any industrial uses of proof assistants?
added by Anton Trunov Nov 20 at 8:47
link|flag
up vote 12 down vote
What is small-scale reflection (as in SSReflect) and how is it different from other types of reflection?
added by Anton Trunov Nov 20 at 11:17
link|flag
up vote 11 down vote
Why do some unification algorithms for dependent matching lead to k axiom?
added by Tiago Campos Nov 20 at 1:18
link|flag
up vote 11 down vote
Have ideas of formal proof assistants been used in areas other than math and CS, e.g. physics?
added by Mario Krenn Nov 20 at 2:08
link|flag
up vote 11 down vote
What are the challenges arising from attempts to integrate intuitionistic theorem provers with SMT solvers?
added by Anton Trunov Nov 20 at 8:09
link|flag
up vote 10 down vote
Agda often inserts fully qualified names on `C-c C-c`, e.g., `Some.Module.foo` instead of `foo`, where `Some.Module` is opened. Is there a fix?
added by Andrej Bauer Nov 19 at 21:39
link|flag
up vote 10 down vote
How do I create a list of graphs in Lean? All elements of a list must share the same type, but graphs depend on their vertex types.
added by Andrej Bauer Nov 19 at 21:47
link|flag
up vote 10 down vote
What is the difference between "Locale" in Isabelle/HOL and dependent records in MLTT?
added by ice1000 Nov 19 at 22:38
link|flag
Just a fine point: the prover platform is called "Isabelle", its core logic is called "Isabelle/Pure", and its main library of theories and proof tools happens to be "Isabelle/HOL". Locales are a concept of Isabelle/Pure: thus they also work with non-HOL applications. – Makarius Nov 20 at 19:22
up vote 10 down vote
Can induction be proved for λ-encoded datatypes?
added by Dokkat Nov 19 at 22:38
link|flag
up vote 10 down vote
How can addition associativity be proven in each proof assistant?
added by Dokkat Nov 19 at 22:42
link|flag
up vote 10 down vote
Is there a way to automatically derive the "obvious" equivalence between types in Lean?
added by Kyle Miller Nov 19 at 22:50
link|flag
up vote 10 down vote
Where can I find benchmarks comparing the performance of various proof assistants?
added by gallais Nov 19 at 22:55
link|flag
up vote 10 down vote
How can I rewrite this `fintype.card`? Lean says "motive is not type correct."
added by Kyle Miller Nov 19 at 22:56
link|flag
More generally: what are good general guidelines for dealing with "motive is not type correct" – Neil Strickland Nov 20 at 7:20
up vote 10 down vote
How do we Church-encode (or in any other lambda encoding styles) inductive-recursive types?
added by ice1000 Nov 19 at 23:05
link|flag
up vote 10 down vote
For mathlib, what's the right list of typeclasses and hypotheses to introduce a vector space over a field of characteristic 0?
added by Kyle Miller Nov 19 at 23:13
link|flag
up vote 10 down vote
Can I avoid having a universe bump with this inductive type?
added by Kyle Miller Nov 19 at 23:21
link|flag
You might want to mention which proof assistant this question is about (e.g., Lean) in the title. – tophat Nov 20 at 19:06
2  
I asked it this way since I imagined there would be tags for each proof assistant on the real site, but perhaps the community convention will be to include the proof assistant in the title regardless. – Kyle Miller Nov 20 at 19:32
up vote 10 down vote
Why Agda's `--without-K` option also affects the indices of inductive types, where they have to be of smaller sizes?
added by ice1000 Nov 19 at 23:24
link|flag
up vote 10 down vote
I'm having trouble mixing universe polymorphism and modules in Coq. Why do I seem to need to specify monomorphic universes in this case?
added by Molossus Spondee Nov 19 at 23:32
link|flag
up vote 10 down vote
What are some useful resources for a mathematician interested in learning Isabelle/HOL?
added by Kevin Buzzard Nov 19 at 23:53
link|flag
2  
This would probably be a good question in the early stages of the site. Later on, I suspect the questions would become more specific. – Andrej Bauer Nov 19 at 23:59
up vote 10 down vote
What more is there in the Lean ecosystem around formalizing math besides mathlib?
added by Greg Nov 20 at 0:47
link|flag
up vote 10 down vote
Does Lean 4 offer any way to reinstate support for homotopy type theory?
added by Greg Nov 20 at 0:50
link|flag
up vote 10 down vote
Is there a consolidated list of backward-incompatible changes in Lean's mathlib, to help people trying to update old code?
added by Neil Strickland Nov 20 at 7:18
link|flag
up vote 10 down vote
Is there any formulation of univalence relating types of different universe levels? So that we can transport universe polymorphic properties.
added by Kang Rongji Nov 20 at 8:20
link|flag
up vote 10 down vote
What is/are the non-trivial difference(s) between Computer Algebra Systems and Proof Assistants?
added by prash Nov 20 at 10:07
link|flag
up vote 10 down vote
Which proof assistants can also serve as general-purpose programming languages?
added by bbarker Nov 20 at 12:06
link|flag
up vote 10 down vote
Are there proof assistants that come with a well-maintained formal specification and mechanized metatheory of their own type theory?
added by k4rtik Nov 20 at 12:57
link|flag
up vote 10 down vote
What's the difference between Coq's Prop, Idris' quantity 0, and Agda's various flavours of irrelevance?
added by gallais Nov 20 at 14:30
link|flag
up vote 10 down vote
Can I trust a compiled proof (e.g. .vo, .agdai, or .ttc file) provided by an adversary?
added by gallais Nov 20 at 14:32
link|flag
up vote 10 down vote
Can I connect a proof assistant with a computer algebra system such as Mathematica or Maple?
added by Andrej Bauer Nov 20 at 16:19
link|flag
up vote 10 down vote
Is it legitimate to use Coq's Prop in HoTT/UF proofs?
added by Martín Hötzel Escardó Nov 20 at 16:42
link|flag
1 2