User Andrej Bauer

4 votes

Is there a multiway system which is equivalent to taking ZFC as axioms?

answered Nov 20 at 12:22

2 votes

Accepted

problem with unification

answered Nov 18 at 9:20

6 votes

Universe inconsistency errors when using ZF model in Coq

answered Nov 8 at 1:00

10 votes

Accepted

What is a deep embedding vs a shallow embedding? With examples?

answered Oct 13 at 22:01

3 votes

(Dis)Advantages of basing a proof assistant on CH correspondence?

answered Sep 19 at 13:04

1 vote

confused about stlc from Programming Language Foundations

answered Sep 6 at 19:02

2 votes

What is the type-in-type problem in idris2 and can it be avoided?

answered Aug 26 at 8:28

3 votes

Can we prove every provable statement with Lean?

answered Aug 15 at 16:48

3 votes

Accepted

How to reason about and extract code for inductive types with negative occurrences in Coq?

answered Aug 15 at 7:37

5 votes

Accepted

Coq: Would adding "inline inductive definition expressions" introduce inconsistency?

answered Aug 9 at 8:52

2 votes

Accepted

New types in higher order logic

answered Aug 5 at 9:29

1 vote

How do I extract efficient string code in Coq to OCaml?

answered Jul 15 at 9:05

2 votes

What if identity type in extensional type theory were possibly non-deterministic?

answered Jul 15 at 8:02

5 votes

Partitioning a list with 2 elements in the middle in coq

answered Jul 13 at 9:19

3 votes

How does one show termination of a function that is structurally recursive over a type T with subterms of type List T?

answered Jul 8 at 10:37

16 votes

Have ideas from programming helped us create new mathematical proofs?

answered Jul 5 at 15:58

0 votes

Accepted

Existential quantification on types in Isabelle

answered Jul 3 at 19:20

4 votes

Accepted

Feferman's universes for proof assistants?

answered Jun 28 at 12:51

5 votes

Accepted

Is there a most flexible type theory or proof assistant?

answered Jun 19 at 16:24

1 vote

Inspecting proof terms in Agda

answered Jun 15 at 21:33

3 votes

Accepted

Can alg be used for the formal semantics of a language?

answered Jun 10 at 9:24

5 votes

Accepted

Pattern matching from `Prop` to `Type` in Lean

answered Jun 4 at 12:27

2 votes

Accepted

Recursive definition of a sum of squares

answered Jun 3 at 14:54

3 votes

Accepted

How to encode and manipulate (parallel) substitutions?

answered Jun 1 at 21:10

5 votes

Accepted

Auxiliary Typeclasses in Lean

answered May 30 at 8:05

3 votes

Abstracting over large types in type theory

answered May 26 at 11:24

3 votes

How does Z3 "exhaustively search" real numbers?

answered May 25 at 13:31

2 votes

Accepted

State-of-the-art constructive encodings of Reals in a (constructive) type theory that supports quotient-types

answered May 21 at 10:02

5 votes

I'm stuck trying to prove ∀x : ℕ, 3 | (x + 5x) with Coq

answered May 12, 2022 at 6:22

18 votes

Accepted

What's the difference between reflection and tactics?

answered Mar 20, 2022 at 9:48

Stack Exchange Network

101 Answers

Is there a multiway system which is equivalent to taking ZFC as axioms?

problem with unification

Universe inconsistency errors when using ZF model in Coq

What is a deep embedding vs a shallow embedding? With examples?

(Dis)Advantages of basing a proof assistant on CH correspondence?

confused about stlc from Programming Language Foundations

What is the type-in-type problem in idris2 and can it be avoided?

Can we prove every provable statement with Lean?

How to reason about and extract code for inductive types with negative occurrences in Coq?

Coq: Would adding "inline inductive definition expressions" introduce inconsistency?

New types in higher order logic

How do I extract efficient string code in Coq to OCaml?

What if identity type in extensional type theory were possibly non-deterministic?

Partitioning a list with 2 elements in the middle in coq

How does one show termination of a function that is structurally recursive over a type T with subterms of type List T?

Have ideas from programming helped us create new mathematical proofs?

Existential quantification on types in Isabelle

Feferman's universes for proof assistants?

Is there a most flexible type theory or proof assistant?

Inspecting proof terms in Agda

Can alg be used for the formal semantics of a language?

Pattern matching from `Prop` to `Type` in Lean

Recursive definition of a sum of squares

How to encode and manipulate (parallel) substitutions?

Auxiliary Typeclasses in Lean

Abstracting over large types in type theory

How does Z3 "exhaustively search" real numbers?

State-of-the-art constructive encodings of Reals in a (constructive) type theory that supports quotient-types

I'm stuck trying to prove ∀x : ℕ, 3 | (x + 5x) with Coq

What's the difference between reflection and tactics?