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

2 votes
0 answers
27 views

Problem working with FMapWeakList and Parametrized Records

1 vote
1 answer
138 views

how to prove 2+2+a=4+a in lean4?

1 vote
1 answer
88 views

confused about stlc from Programming Language Foundations

1 vote
0 answers
57 views

Embedding proof assistance in an application

1 vote
1 answer
68 views

Recursive type class for OfNat Even

2 votes
1 answer
78 views

Metamath unification example

1 vote
1 answer
56 views

İnduction/inversion and others in coq

2 votes
1 answer
247 views

How to install dependencies correctly? [Cannot find a physical path bound to logical path]

44 votes
9 answers
5k views

Proof assistants for beginners - a comparison

2 votes
1 answer
80 views

How do I do for-all introduction in Isabelle?

2 votes
1 answer
53 views

Proving a logic riddle in Coq : testing equivalence in an Inductive set

0 votes
1 answer
60 views

Reasoning about non reflexive equalities & type conversions

1 vote
3 answers
138 views

How do I express a fixpoint of a decreasing argument that is not a subterm of the function's argument?

0 votes
1 answer
102 views

What is the idiomatic way in Coq to write recursive functions over product types?

Browse more Questions