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

3 votes
2 answers
186 views

Universe inconsistency errors when using ZF model in Coq

5 votes
1 answer
452 views

Examples of theories where tactic language is required for simple proofs

0 votes
2 answers
179 views

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

2 votes
1 answer
164 views

What is a pattern in dependent pattern matching?

4 votes
1 answer
93 views

What is the best way to learn Iris completely independently

0 votes
1 answer
127 views

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

2 votes
1 answer
138 views

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

2 votes
2 answers
93 views

Continue a section (with context) in coq

2 votes
1 answer
111 views

Are all LEAN tactics equivalent to applying some theorem?

2 votes
1 answer
97 views

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

2 votes
2 answers
68 views

metamath meta variables

1 vote
1 answer
79 views

problem with unification

1 vote
2 answers
80 views

How to introduce assumption in lean4

1 vote
1 answer
57 views

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

0 votes
1 answer
65 views

How to run lean4 with mathlib manually

1 vote
0 answers
63 views

Unfolding constants while rewriting using rewrite_strat and a hint database

0 votes
0 answers
50 views

How to check a Zenon-generated proof with Coq?

2 votes
0 answers
26 views

Problem working with FMapWeakList and Parametrized Records

0 votes
0 answers
15 views

reference ospecialize and variable prim_base_irreducible not found in the current environment


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