Stack Exchange
log in sign up chat discuss faq users badges

Area 51 » Science

definition commitment beta
238
followers
Share This

Proof Assistants

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

0
votes
0
answers

Could we use a Stack Overflow Collective for Proof Assistants?

mar 11 at 19:07 V2Blast♦ 186
25
votes
6
answers

Are automatic theorem provers on-topic?

jan 29 at 18:05 Molossus Spondee 251
27
votes
1
answer

Proof Assistants' finalized launch date, name, and URL

jan 28 at 14:23 Dima Pasechnik 151
27
votes
1
answer

Proof Assistants private beta launch will take place in February 2022

jan 27 at 15:37 JNat♦ 299
33
votes
10
answers

Choosing a name for the Proof Assistants site

jan 27 at 15:08 Guy Coder 1,746

show 8 more discussions
discuss this proposal

This proposal is now in the Beta 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 '21 at 21:36
link
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 '21 at 23:52
link
up vote 18 down vote
Why, after all these years, is append not obviously associative?
added by pigworker Nov 19 '21 at 21:40
link
3  
More of a comment than a question, amirite? – Cactus Nov 20 '21 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 '21 at 4:34
link
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 '21 at 23:28
link
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 '21 at 11:23
link
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 '21 at 21:52
link
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 '21 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 '21 at 22:25
Yes, I agree it need not be specific to a particular proof-assistant. – Andrej Bauer Nov 19 '21 at 22:32
4  
(answer to real question is "yes in Lean: leanprover-community.github.io/mathlib_docs/…) – Kevin Buzzard Nov 19 '21 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 '21 at 22:25
link
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 '21 at 22:44
link
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 '21 at 8:06
link
up vote 12 down vote
Any industrial uses of proof assistants?
added by Anton Trunov Nov 20 '21 at 8:47
link
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 '21 at 11:17
link
up vote 11 down vote
Why do some unification algorithms for dependent matching lead to k axiom?
added by Tiago Campos Nov 20 '21 at 1:18
link
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 '21 at 2:08
link
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 '21 at 8:09
link
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 '21 at 21:39
link
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 '21 at 21:47
link
up vote 10 down vote
What is the difference between "Locale" in Isabelle/HOL and dependent records in MLTT?
added by ice1000 Nov 19 '21 at 22:38
link
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 '21 at 19:22
up vote 10 down vote
Can induction be proved for λ-encoded datatypes?
added by Dokkat Nov 19 '21 at 22:38
link
up vote 10 down vote
How can addition associativity be proven in each proof assistant?
added by Dokkat Nov 19 '21 at 22:42
link
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 '21 at 22:50
link
up vote 10 down vote
Where can I find benchmarks comparing the performance of various proof assistants?
added by gallais Nov 19 '21 at 22:55
link
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 '21 at 22:56
link
More generally: what are good general guidelines for dealing with "motive is not type correct" – Neil Strickland Nov 20 '21 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 '21 at 23:05
link
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 '21 at 23:13
link
up vote 10 down vote
Can I avoid having a universe bump with this inductive type?
added by Kyle Miller Nov 19 '21 at 23:21
link
You might want to mention which proof assistant this question is about (e.g., Lean) in the title. – tophat Nov 20 '21 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 '21 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 '21 at 23:24
link
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 '21 at 23:32
link
up vote 10 down vote
What are some useful resources for a mathematician interested in learning Isabelle/HOL?
added by Kevin Buzzard Nov 19 '21 at 23:53
link
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 '21 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 '21 at 0:47
link
up vote 10 down vote
Does Lean 4 offer any way to reinstate support for homotopy type theory?
added by Greg Nov 20 '21 at 0:50
link
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 '21 at 7:18
link
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 '21 at 8:20
link
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 '21 at 10:07
link
up vote 10 down vote
Which proof assistants can also serve as general-purpose programming languages?
added by bbarker Nov 20 '21 at 12:06
link
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 '21 at 12:57
link
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 '21 at 14:30
link
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 '21 at 14:32
link
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 '21 at 16:19
link
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 '21 at 16:42
link
1 2 next

This site is in

Public Beta

Anyone can participate!

Sites remain in beta for at least 90 days to build up a critical mass of users, questions, and participation.

proposed by

Andrej Bauer
112k●13●302●578

6 months ago

edited by

Henry WH Hack v3.0b
8,821●13●65●156

6 months ago

viewed

13,889 times

latest activity

3 months ago

followers

users also following

1.3% TeX, LaTeX and fr...
1.3% Mathematics
1.3% Theoretical Compu...
1.3% Bioacoustics
79.8% only this proposal

followers active in

37.8% Stack Overflow
27.3% Mathematics
21.8% Proof Assistants
18.9% MathOverflow
16.0% TeX - LaTeX
12.2% Theoretical Compu...

recent followers

added Feb 11 at 17:35
Nike Dattani
70.1k●11●258●847
added Jan 23 at 8:48
Jake Symons
1,253●3●17●41
added Jan 20 at 16:35
მამუკა ჯიბლაძე
22.2k●3●111●262
added Jan 20 at 16:16
Mamuka Jibladze
51●1
added Jan 17 at 20:31
Dustin G. Mixon
11.3k●2●38●97
added Dec 23 '21 at 21:05
Pyautogui
1,730●6●42
added Dec 17 '21 at 2:57
Jon Bannon
17.3k●10●122●220
added Dec 13 '21 at 23:47
finitud
1,112●1●6●24
added Dec 13 '21 at 7:17
Beleg
473●1●8
added Dec 10 '21 at 18:56
Serkan Dereli
51●1
added Dec 10 '21 at 14:49
user217834
51●1
added Dec 2 '21 at 7:58
Gergely
11.6k●10●63●163
added Dec 1 '21 at 23:18
Åsmund Kløvstad
51●1
added Nov 30 '21 at 15:39
user217403
51●1
added Nov 30 '21 at 12:09
Wheat Wizard ♦ 1
100k●20●315●811
added Nov 29 '21 at 11:46
Shreck Ye
1,522●1●12●29
added Nov 28 '21 at 0:37
ErikMD
10.9k●2●27●68
added Nov 27 '21 at 6:58
MarnixKlooster ReinstateMonica
16.8k●21●96●211
added Nov 24 '21 at 8:41
Björn Brandenburg
51●2
added Nov 24 '21 at 0:47
user458276
1,928●1●7●31
added Nov 23 '21 at 17:39
user217198
51●1
added Nov 23 '21 at 15:13
Pedro Sánchez Terraf
6,356●3●24●73
added Nov 23 '21 at 10:16
The Amplitwist
3,970●6●31●77
added Nov 23 '21 at 10:15
A Rogue Ant
35.6k●16●137●314
added Nov 23 '21 at 7:10
user217160
51●1
added Nov 23 '21 at 2:04
Huỳnh Trần Khanh
51●1
added Nov 23 '21 at 0:48
Jia Ming
2,177●1●13●42
added Nov 22 '21 at 21:10
ionchy
2,197●4●13●49
added Nov 22 '21 at 20:15
Alexander Kogtenkov
6,293●1●31●46
added Nov 22 '21 at 19:24
Samuel Gruetter
51●1
added Nov 22 '21 at 15:55
Couchy ♦ 1
5,121●3●22●85
added Nov 22 '21 at 13:35
user217105
51●1
added Nov 22 '21 at 4:48
Bubbler
76.4k●5●157●506
added Nov 21 '21 at 22:21
vikraman
780●8●21
added Nov 21 '21 at 20:26
rj00a
51●1
added Nov 21 '21 at 14:14
Jörg
51●1●1
added Nov 21 '21 at 13:27
user9716869
3,623●2●22●55
added Nov 21 '21 at 11:28
Cheery
24.2k●15●61●112
added Nov 21 '21 at 9:30
fosco
23.8k●3●71●145
added Nov 21 '21 at 6:07
David Roberts
39.9k●10●167●412
feed icon proposal feed
faq | blog | legal | privacy policy | contact us | feedback always welcome
site design / logo © 2022 Stack Exchange Inc; user contributions licensed under cc by-sa; see the licensing help page for more information.
rev 2022.3.23.593