Skip to main content

Top Questions

4 votes
1 answer
291 views

In ITT, are all provable equalities in the empty context provable by refl?

0 votes
0 answers
26 views

How to fix SPASS GUI editor bug

0 votes
1 answer
37 views

How to find a substring in a string in Lean 4?

0 votes
0 answers
61 views

How to use Lean to generate a program in python?

3 votes
2 answers
382 views

Proving an order relation between two concrete real numbers (Lean)

9 votes
2 answers
931 views

What efforts have there been in trying to automate diagrammatic proofs in category theory?

3 votes
1 answer
147 views

Why is Lean4 an intensional type theory?

0 votes
1 answer
112 views

Proof of completeness theorem in first order logic

1 vote
1 answer
67 views

Matching Singleton Sets in Lean4

2 votes
1 answer
47 views

Error using equality with type Rational in Lean 4?

1 vote
3 answers
123 views

Mathcomp's all_ssreflect prevents from compiling

0 votes
0 answers
44 views

Reasoning About TAPL Unification in Rocq

3 votes
0 answers
86 views

What's the current state of the art in the formalisation of spectral sequence arguments in Lean?

4 votes
1 answer
131 views

What is the standard equivalent of an Ltac match in lean4?

2 votes
2 answers
93 views

Data structure for context in STLC

1 vote
1 answer
96 views

Prove an inequality in Rocq

5 votes
2 answers
170 views

Comparison of expressive power of GADTs and Inductive types

2 votes
1 answer
156 views

Prove bisimilarity of coinductive streams

3 votes
1 answer
127 views

Is there a model that contradicts `@eq Type t1 t2 -> @eq Prop t1 t2` or can it be proven?

1 vote
1 answer
126 views

What is Isabelle's new antiquotation syntax for cite?

1 vote
0 answers
88 views

What is the status of Software Foundations ports to Lean 4, and what is the canonical alternative?

2 votes
0 answers
61 views

Wanted: API for theorem prover

0 votes
1 answer
59 views

Small step reduction of terms with saving intermediate results

0 votes
0 answers
47 views

How to use the lean4 syntax/macro rules in BNF style?

0 votes
1 answer
85 views

How to coerce/convert constant to the type of a given variable?

2 votes
2 answers
228 views

What it takes to formalize concrete models of ∞-categories in Lean 4, e.g. like rzk approach using 3-level type theory?

2 votes
1 answer
86 views

Isabelle "by" and "." magic for Pure "⟹" inference

3 votes
3 answers
212 views

What is an assumption in Isar?

29 votes
3 answers
2k views

What set-theoretic definitions can't easily be formalized in a type theory?

0 votes
1 answer
172 views

Coq - Overloading over multiple parameters with canonical structures

7 votes
3 answers
323 views

Is there an easy-to-learn GUI of proof assistants for teenagers in maths education?

23 votes
1 answer
358 views

What is known about performance bottlenecks in proof assistants?


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