Skip to main content
Andrej Bauer's user avatar
Andrej Bauer's user avatar
Andrej Bauer's user avatar
Andrej Bauer
  • Member for 2 years, 4 months
  • Last seen this week
3 votes

Can we prove every provable statement with Lean?

3 votes

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

3 votes
Accepted

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

3 votes

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

3 votes
Accepted

How to encode and manipulate (parallel) substitutions?

3 votes

How does Z3 "exhaustively search" real numbers?

3 votes

Abstracting over large types in type theory

3 votes

Creating a proof assistant for first order logic in Haskell

3 votes

Is there a tactic in Coq to make a hypothesis from applying two hypotheses?

2 votes

Coq: can `tauto` be used to prove classical tautologies?

2 votes
Accepted

How do you implement what's in the Pierce Book precisely? And why / why not have evaluation just mutate ParseTree's of a PEG parser generator library?

2 votes

Natural deduction vs simply typed lambda calculus

2 votes
Accepted

Recursive definition of a sum of squares

2 votes
Accepted

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

2 votes

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

2 votes
Accepted

New types in higher order logic

2 votes
Accepted

problem with unification

2 votes

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

2 votes

Proof Assistants in OOP languages

2 votes
Accepted

Is the validity of induction in Coq axiomatic?

2 votes

Topic for undergraduate thesis

2 votes

How to implement separate compilation?

1 vote

How can I reason backwards and assume the conclusion holds in Lean 4?

1 vote

How do I define an induction principle for a type with a nested list of tuples?

1 vote

Defining and using bisimilarity for negatively-defined conatural numbers

1 vote

How exactly solved metas "revisited" in an efficient dependent type checker?

1 vote
Accepted

Verifying a basic function with Lean4

1 vote

confused about stlc from Programming Language Foundations

1 vote
Accepted

What are deductive systems associated with raw type theories?

1 vote
Accepted

In lean4 why is induction only rewriting the goal, and not the known facts?