Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.

Sign up to join this community
Anybody can ask a question
Anybody can answer
The best answers are voted up and rise to the top

Explore our questions

1 vote
0 answers
46 views

Implementation of cubical type theory as described in this paper?

1 vote
1 answer
54 views

Lean 4: How can I specify that out of two universe variables, one is larger than the other?

1 vote
4 answers
256 views

How to to use the fact that combining these hypothesis is false in Coq

-2 votes
1 answer
45 views

Lean prediacte logic problem. existentially quantified proposition

0 votes
0 answers
24 views

How to read/understand the definition of the environment in type-checking?

0 votes
1 answer
45 views

Proof of Constant folding in Coq for IMP using Interaction Trees

-2 votes
1 answer
32 views

plz any guide me for coq extension in VS code

0 votes
1 answer
92 views

A CoQ program which constructively proves the halting problem

0 votes
0 answers
19 views

Coq makefile complains about extension points on Windows 10

-2 votes
0 answers
26 views

Using verdi raft. How do I import it into my Coq Project?

2 votes
1 answer
346 views

Why is lean 4 behaving differently on my machine vs in the natural number game?

-1 votes
0 answers
48 views

Lean predicate logic . Error in my proof , could anyone help?

0 votes
3 answers
191 views

LEM, the halting problem, the curry-howard correspondence -> deep connection?

0 votes
1 answer
69 views

What is the difference between these inductive definitions in Coq?

Browse more Questions