Skip to main content

Explore our questions

0 votes
0 answers
1 view

Simple and cheap proof assistants for everyone? Base2 as a case study

1 vote
1 answer
150 views

Coq ssreflect - rewrite inside \big

6 votes
1 answer
258 views

How far is Gentzen's consistency proof of Peano Arithmetic from being formalized?

0 votes
0 answers
50 views

Stuck proving the induction hypothesis of multiplication on natural numbers mul_n_S?

2 votes
1 answer
258 views

A list with relations between elements in Lean

0 votes
1 answer
125 views

Defining and Instantiating Functors with Partially Defined Members

0 votes
1 answer
115 views

Fixing made up QuotientMap in ProofNet, what is the recommended name?

2 votes
1 answer
95 views

A strange issue with a type alias in Lean4

1 vote
2 answers
88 views

Write a Ltac that exploits the order of declaration

0 votes
1 answer
83 views

Construct the sum of reals indexing on a finType

1 vote
1 answer
210 views

Reverse Mathematics: An Avenue Worth Exploring?

0 votes
1 answer
358 views

What strategy should I learn to generalize my observations?

2 votes
1 answer
310 views

Locally downloaded Mathlib files not being accessed by Lean

0 votes
0 answers
102 views

What is exactly _pattern_value_ in Rocq?

Browse more Questions