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

0 votes
0 answers
2 views

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

2 votes
1 answer
320 views

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

0 votes
0 answers
6 views

Coq makefile complains about extension points on Windows 10

-1 votes
0 answers
20 views

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

0 votes
3 answers
134 views

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

0 votes
1 answer
51 views

What is the difference between these inductive definitions in Coq?

2 votes
2 answers
47 views

Shortening a 4-levels-of-match lean4 proof of the CHSH inequality

0 votes
1 answer
51 views

Alpha equivalent subgoals

0 votes
1 answer
17 views

In lean 4, how do I give names to variables when using `split`?

0 votes
1 answer
24 views

In lean 4, how do I refer to variables with names like `a✝`

0 votes
1 answer
34 views

What do I need to import from MathLib to make `induction a with d hd` work?

0 votes
0 answers
28 views

Integrating SAT solvers supporting only a finite set of variables into proof assistants

3 votes
1 answer
80 views

Print the version of lean that is running

0 votes
1 answer
41 views

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

Browse more Questions