Skip to main content

Explore our questions

3 votes
0 answers
17 views

Formalization of constructive books

1 vote
0 answers
15 views

Defining Brownian Motion in Lean4

1 vote
1 answer
80 views

Can this Free Logic prove everything ZFC can?

2 votes
1 answer
110 views

How to use Modus Ponens in L axiomatic system

5 votes
1 answer
316 views

Could Prop be the top universe?

2 votes
1 answer
88 views

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

5 votes
2 answers
441 views

Is there a complete index of Lean 4 tactics?

3 votes
1 answer
85 views

Extensional sets in Coq and induction

3 votes
1 answer
292 views

Natural deduction with coq assistant prover

5 votes
0 answers
97 views

The hypercompleteness swindle

3 votes
1 answer
94 views

Stochastic calculus in Lean4?

4 votes
1 answer
385 views

How does Coq guess `i` is decreasing?

3 votes
2 answers
275 views

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

1 vote
1 answer
25 views

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

Browse more Questions