User Andrej Bauer

32 votes

Accepted

What is predicativity?

answered Feb 11, 2022 at 10:07

31 votes

Accepted

In Lean, what do double curly brackets mean?

answered Feb 8, 2022 at 20:43

31 votes

Accepted

What set-theoretic definitions can't easily be formalized in a type theory?

answered Feb 9, 2022 at 21:50

28 votes

Accepted

What is an algebraic data type?

answered Feb 28, 2022 at 8:51

25 votes

Accepted

Non-trivial difference(s) between Computer Algebra System and Proof Assistant

answered Feb 8, 2022 at 21:56

19 votes

Accepted

How to extract the witness from exists in Coq in function notation/without destructing?

answered Apr 24, 2022 at 14:22

18 votes

Accepted

Do you need a Hilbert style Epsilon operator for definitions in set theory?

answered Apr 30, 2022 at 6:41

18 votes

Accepted

What work has been done on computationally intensive proofs?

answered Mar 26, 2022 at 9:49

18 votes

Accepted

How to run Agda?

answered Feb 8, 2022 at 21:16

18 votes

Accepted

Tools for checking the consistency of a type theory

answered Feb 20, 2022 at 22:28

18 votes

Why is cumulativity not a given in proof assistants?

answered Feb 19, 2022 at 22:24

17 votes

How can I prove facts about floating point calculations?

answered Feb 8, 2022 at 22:35

17 votes

Where can I find lists of theorems that have been verified?

answered Feb 9, 2022 at 6:56

17 votes

Accepted

What's the difference between reflection and tactics?

answered Mar 20, 2022 at 9:48

16 votes

Impact of "Formalizing 100 Theorems" and what is next

answered Feb 12, 2022 at 16:55

15 votes

Proof Assistants with support for creating executable software artifacts

answered Feb 8, 2022 at 21:07

14 votes

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

answered Feb 13, 2022 at 17:53

14 votes

Accepted

What is the role of impredicativity in program extraction?

answered Mar 31, 2022 at 21:07

14 votes

Open source proof assistants for first order logic with equality and set theory

answered Jun 15, 2022 at 5:55

13 votes

Can theorem provers be used to form foundations for programming languages?

answered Feb 9, 2022 at 21:59

13 votes

Accepted

Can mathematical formalizations in NuPRL be trusted as correct in the greater mathematical practice?

answered Mar 11, 2022 at 7:25

12 votes

Accepted

What's “conservativity” in terms of type theory and how is it useful?

answered Feb 27, 2022 at 9:19

12 votes

Can the development of proof assistants make mathematicians switch their framework?

answered Feb 18, 2022 at 9:16

12 votes

What are the pros and cons of continuous checking over keychord-triggered checking?

answered Feb 19, 2022 at 17:12

11 votes

What is known about the consistency of proof assistant metatheories?

answered Mar 2, 2022 at 14:52

10 votes

Formalizations of unsolved problems

answered Mar 22, 2022 at 16:52

9 votes

Accepted

Given `A = B`, how to prove `a: A` also has type B in Lean 4

answered Sep 20, 2022 at 7:59

9 votes

Accepted

Strong induction on ℕ with function α → ℕ

answered Mar 14, 2022 at 23:03

9 votes

Accepted

Attempts to accommodate theories of different consistency strength in single assistant

answered Feb 12, 2022 at 16:45

8 votes

Accepted

Are eliminators useful in practice, or are they only useful in the metatheory?

answered Feb 12, 2022 at 7:34

Stack Exchange Network

79 Answers

What is predicativity?

In Lean, what do double curly brackets mean?

What set-theoretic definitions can't easily be formalized in a type theory?

What is an algebraic data type?

Non-trivial difference(s) between Computer Algebra System and Proof Assistant

How to extract the witness from exists in Coq in function notation/without destructing?

Do you need a Hilbert style Epsilon operator for definitions in set theory?

What work has been done on computationally intensive proofs?

How to run Agda?

Tools for checking the consistency of a type theory

Why is cumulativity not a given in proof assistants?

How can I prove facts about floating point calculations?

Where can I find lists of theorems that have been verified?

What's the difference between reflection and tactics?

Impact of "Formalizing 100 Theorems" and what is next

Proof Assistants with support for creating executable software artifacts

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

What is the role of impredicativity in program extraction?

Open source proof assistants for first order logic with equality and set theory

Can theorem provers be used to form foundations for programming languages?

Can mathematical formalizations in NuPRL be trusted as correct in the greater mathematical practice?

What's “conservativity” in terms of type theory and how is it useful?

Can the development of proof assistants make mathematicians switch their framework?

What are the pros and cons of continuous checking over keychord-triggered checking?

What is known about the consistency of proof assistant metatheories?

Formalizations of unsolved problems

Given `A = B`, how to prove `a: A` also has type B in Lean 4

Strong induction on ℕ with function α → ℕ

Attempts to accommodate theories of different consistency strength in single assistant

Are eliminators useful in practice, or are they only useful in the metatheory?