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

Top Questions

0 votes
0 answers
2 views

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

2 votes
1 answer
319 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
133 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?

2 votes
1 answer
54 views

Apply `unfold` once, instead of many times, in lean4

1 vote
1 answer
157 views

How do I make the rational numbers 0 and 1/2 in lean4?

1 vote
1 answer
27 views

Case assumption missing from tactic state in lean4

1 vote
1 answer
86 views

How to run lean4 with mathlib manually

1 vote
1 answer
50 views

Rewriting certain terms in Lean4

3 votes
1 answer
47 views

Particularization in algebraic statements in Isabelle

1 vote
0 answers
71 views

Any study about negative existentials?

9 votes
2 answers
470 views

What is the state of the art in proof automation in HoTT/CuTT?

3 votes
0 answers
35 views

Verify maximal diameter of a tree in Dafny

5 votes
2 answers
204 views

What is a context mapping in dependent type checking?

6 votes
1 answer
431 views

Paths Between Quotient Types in Cubical Agda

2 votes
1 answer
185 views

What is a pattern in dependent pattern matching?

27 votes
3 answers
785 views

How to search for an existing theorem in Lean?

2 votes
2 answers
73 views

metamath meta variables

5 votes
0 answers
213 views

Mere propositions and Consistency with Impredicativity, Excluded Middle and Large Elimination

0 votes
2 answers
191 views

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

1 vote
0 answers
68 views

Unfolding constants while rewriting using rewrite_strat and a hint database

4 votes
1 answer
106 views

What is the best way to learn Iris completely independently

0 votes
0 answers
16 views

reference ospecialize and variable prim_base_irreducible not found in the current environment

1 vote
1 answer
84 views

problem with unification

0 votes
0 answers
56 views

How to check a Zenon-generated proof with Coq?

1 vote
1 answer
63 views

How to express that two equivalence relations can setoid rewrite across each other (Coq)

0 votes
1 answer
131 views

Induction COQ Question

2 votes
1 answer
141 views

Are all LEAN tactics equivalent to applying some theorem?

7 votes
1 answer
221 views

How does Lean `simp` tactic work?

1 vote
2 answers
93 views

How to introduce assumption in lean4

3 votes
2 answers
198 views

Universe inconsistency errors when using ZF model in Coq

7 votes
3 answers
276 views

Preserve equality with match expression

5 votes
1 answer
466 views

Examples of theories where tactic language is required for simple proofs

0 votes
1 answer
134 views

Why inductive types (or variants) are so rigid in terms of the set of constructors

2 votes
1 answer
110 views

How to Prove Theorem le_zero in Lean4: If x ≤ 0, then x = 0?

2 votes
2 answers
93 views

Continue a section (with context) in coq

2 votes
1 answer
148 views

How to understand the sigma types example from "Theorem Proving in Lean 4"?

2 votes
0 answers
27 views

Problem working with FMapWeakList and Parametrized Records


Looking for more? Browse the complete list of questions, or popular tags. Help us answer unanswered questions.