Andrej Bauer's user avatar
Andrej Bauer's user avatar
Andrej Bauer's user avatar
Andrej Bauer
  • Member for 1 year, 7 months
  • Last seen this week
33 votes
Accepted

What is predicativity?

31 votes
Accepted

In Lean, what do double curly brackets mean?

30 votes
Accepted

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

28 votes
Accepted

What is an algebraic data type?

24 votes
Accepted

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

19 votes

Why is cumulativity not a given in proof assistants?

19 votes
Accepted

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

18 votes
Accepted

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

18 votes
Accepted

What's the difference between reflection and tactics?

18 votes
Accepted

What work has been done on computationally intensive proofs?

18 votes
Accepted

Tools for checking the consistency of a type theory

18 votes

How can I prove facts about floating point calculations?

18 votes
Accepted

How to run Agda?

17 votes

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

16 votes

Impact of "Formalizing 100 Theorems" and what is next

16 votes

Have ideas from programming helped us create new mathematical proofs?

15 votes

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

15 votes

Proof Assistants with support for creating executable software artifacts

14 votes
Accepted

What is the role of impredicativity in program extraction?

14 votes

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

13 votes
Accepted

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

12 votes
Accepted

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

12 votes

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

12 votes

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

12 votes

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

11 votes

What is known about the consistency of proof assistant metatheories?

10 votes

Formalizations of unsolved problems

9 votes
Accepted

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

9 votes
Accepted

Strong induction on ℕ with function α → ℕ

9 votes
Accepted

Attempts to accommodate theories of different consistency strength in single assistant