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

2 votes
1 answer
30 views

What is the precise meaning of "reducible"?

1 vote
1 answer
81 views

Lean: what does the syntax `variable [ring R]` mean?

2 votes
0 answers
67 views

How does Lean `simp` tactic work?

2 votes
0 answers
34 views

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

2 votes
1 answer
139 views

(Dis)Advantages of basing a proof assistant on CH correspondence?

2 votes
1 answer
31 views

How to prove across language boundaries about functions written in another language via FFI?

3 votes
1 answer
247 views

Does lean 4 have built-in dictionary types?

4 votes
1 answer
87 views

Why can addition be used in pattern matching Nats but not multiplication

4 votes
4 answers
427 views

Defining a terminating `ripple`, with arguments swapping places

1 vote
1 answer
61 views

Where do I prove that a return type is valid?

1 vote
0 answers
76 views

Lean proofs for graph algorithms

2 votes
1 answer
71 views

Metamath unification example

3 votes
2 answers
564 views

proof of termination for zip in Lean

1 vote
1 answer
69 views

Result contains obtained parameters? So what?

1 vote
1 answer
42 views

Recursive type class for OfNat Even

1 vote
1 answer
47 views

confused about stlc from Programming Language Foundations

2 votes
1 answer
111 views

Provable `fun-ext`and "rewriting under binders" in intensional MLTT

1 vote
1 answer
42 views

Eliminating dependent destruction in Coq

0 votes
0 answers
29 views

Why does Program Fixpoint leave behind a temporary_proof2_subproof axiom in this example?

0 votes
1 answer
36 views

proof-based Pos type class

1 vote
1 answer
158 views

Formalization of a model of ∞-category in a proof assistant

1 vote
2 answers
63 views

Defining a Recursive Function decreasing on one argument with < and another structurally

0 votes
1 answer
53 views

Specializing forall quantifiers in Coq

1 vote
1 answer
42 views

Typing List.nil

1 vote
1 answer
103 views

Prove an upper bound on the computation time of the Euclidean algorithm in lean4

3 votes
1 answer
100 views

Programming challenge site for lean4

0 votes
0 answers
96 views

Formalization of partial functions for combinatorial counting

2 votes
1 answer
74 views

What is the type-in-type problem in idris2 and can it be avoided?

1 vote
0 answers
92 views

Designing a proof assistant around Cubical

2 votes
0 answers
24 views

Proving (((finset.range 50).erase 0).erase 1).sum id = (finset.range 50).sum id - 1

3 votes
1 answer
56 views

"Expected a single focused goal but 2 goals are focused." error in coq regarding string equality(I think)

2 votes
0 answers
40 views

Factoring custom grammar rules for integers and lists in Coq custom entries

2 votes
1 answer
284 views

Lean 4 Importing into VSCode

2 votes
1 answer
106 views

Rewriting with heterogeneous equality (JMeq)

1 vote
2 answers
117 views

Dependent sum and equality with Coq

2 votes
1 answer
77 views

How to prove a statement about sublists?

6 votes
2 answers
231 views

Lean4 Exercise: Double negation implies law of excluded middle

21 votes
1 answer
383 views

What is the difference between `leanprover` and `leanprover-community` GitHub repositories?

0 votes
1 answer
79 views

Well founded recursion through lists

23 votes
1 answer
502 views

How to search for an existing theorem in Lean?


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