Top Questions

2 votes
3 answers
47 views

Induction on indexed type family without JMeq

0 votes
1 answer
41 views

Coq - Overloading over multiple parameters with canonical structures

1 vote
1 answer
40 views

What is the official way to reinstall Lean4 from scratch on a Mac or Linux?

2 votes
0 answers
86 views

What is the well-established η law for naturals?

0 votes
1 answer
61 views

How does one create a lean project and have mathlib import work when not creating the lean project at the $HOME directory?

3 votes
1 answer
88 views

Stuck in a proof about sum types and nonempty lists

1 vote
1 answer
41 views

Inductively proving that a number is either even or odd in Lean

0 votes
0 answers
18 views

How does one create a lean project even if it already exists e.g., lake +leanprover/lean4:nightly-2023-02-04 new my_project math?

6 votes
2 answers
361 views

Can you have nonstrict positive inductive types predicatively?

3 votes
1 answer
219 views

Determining why my proof depends on the axiom of choice

3 votes
2 answers
71 views

Defining and using bisimilarity for negatively-defined conatural numbers

4 votes
4 answers
478 views

Proof Assistants in OOP languages

6 votes
2 answers
235 views

Lean and inaccessible cardinals

5 votes
1 answer
151 views

What are the principal differences between Agda's core type theory and Coq's?

2 votes
1 answer
27 views

ROOT file for building a heap image in Isabelle

1 vote
1 answer
22 views

Referring to a session properly in another ROOT file in Isabelle

1 vote
1 answer
61 views

Proving that equality is decidable on an ``Inductive Set``

1 vote
3 answers
103 views

Is there a way to incorporate K's axiom while keeping the system consistent with univalence?

3 votes
1 answer
139 views

What are deductive systems associated with raw type theories?

0 votes
1 answer
103 views

A program which could derive theorems given formation rules in any modal logic?

4 votes
2 answers
171 views

Which proof assistants implement Church's rule?

2 votes
1 answer
69 views

Define “vector space” from scratch in Coq

2 votes
2 answers
164 views

How do I prove $\operatorname{succ}(a)$ cannot be equal to $0$ in Lean4?

5 votes
2 answers
112 views

Comparing indexed induction to recursion

3 votes
1 answer
184 views

Selecting both a hypothesis and Goal while applying a tactic

1 vote
1 answer
97 views

Using `decreasing_by` to prove termination in Lean 4

4 votes
0 answers
33 views

Implementing object-logics in Isabelle Best Practices?

0 votes
1 answer
36 views

Is type constraint the same as implication in type space?

2 votes
1 answer
127 views

Is there a way to rename parameters when including/reusing a module type in Coq?

1 vote
0 answers
43 views

Heterogeneous lists, large indices

0 votes
0 answers
115 views

MLTT with first-order reasoning and equality-reasoning information preservation

0 votes
2 answers
254 views

How can I generate equalities from an application in Coq?

0 votes
1 answer
91 views

In Lean 4 how to use an implication in a hypothesis?

1 vote
2 answers
161 views

How to run lean4 with mathlib manually

1 vote
3 answers
250 views

Dependent sum and equality with Coq

1 vote
1 answer
171 views

Equivalence Relations COQ

15 votes
1 answer
732 views

Lean "nonempty" vs "inhabited"

9 votes
2 answers
561 views

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

3 votes
1 answer
137 views

Recursive notations with forall quantifier


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