Skip to main content

Top Questions

1 vote
2 answers
227 views

Why did this proof succeed without function extensionality?

2 votes
1 answer
141 views

Finding reflexive, transitive closure

2 votes
2 answers
83 views

Formalizing "finite or infinite" in Coq

3 votes
1 answer
109 views

How to use SSReflect to prove commutativity and associativity of addition idiomatically?

4 votes
1 answer
102 views

How to perform type conversion/coercion in Lean 4?

1 vote
2 answers
102 views

ACL2: Is there a way to check that a Skolem function does what it says on the tin?

1 vote
1 answer
91 views

Trying to use 'Equations'

0 votes
1 answer
42 views

How to combine the PROP of a list of PROP in lean 4?

1 vote
1 answer
45 views

Applying an axiom from a class in a proof

3 votes
0 answers
57 views

Automatic proofs concerning inequalities

0 votes
1 answer
21 views

Feeding rewrites and other hints into an omnibus tactic

0 votes
0 answers
22 views

Strategies for representing proofs of equality [duplicate]

2 votes
1 answer
18 views

Proper LEAN_PATH environment variable value for Windows Lean Visual Studio project?

2 votes
0 answers
14 views

Use of `by` on first line of lean proof - when to / when not to? [duplicate]


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