Skip to main content

Explore our questions

0 votes
0 answers
13 views

Can this Free Logic prove everything ZFC can?

2 votes
1 answer
95 views

How to use Modus Ponens in L axiomatic system

4 votes
1 answer
276 views

Could Prop be the top universe?

2 votes
1 answer
80 views

Is it possible to simplify/normalize nat arithmetic expressions in Coq?

5 votes
2 answers
437 views

Is there a complete index of Lean 4 tactics?

3 votes
1 answer
84 views

Extensional sets in Coq and induction

3 votes
1 answer
292 views

Natural deduction with coq assistant prover

5 votes
0 answers
94 views

The hypercompleteness swindle

3 votes
1 answer
87 views

Stochastic calculus in Lean4?

4 votes
1 answer
384 views

How does Coq guess `i` is decreasing?

3 votes
2 answers
274 views

What is the unicode braces {| |} (⦃ ... ⦄) in lean 4?

1 vote
1 answer
24 views

Passing functions to casesOn which do not depend on a pattern match

7 votes
2 answers
540 views

Why do some people disagree about whether DTT implies not Turing complete?

2 votes
1 answer
175 views

Could proof assistants fill in single theorems automatically?

Browse more Questions