Skip to main content

Explore our questions

1 vote
2 answers
52 views

Why did this proof succeed without function extensionality?

2 votes
1 answer
79 views

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

4 votes
2 answers
116 views

When is the lean 4 "by" required?

2 votes
0 answers
12 views

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

1 vote
1 answer
90 views

ACL2 compile single book on command line

2 votes
0 answers
51 views

Automatic proofs concerning inequalities

1 vote
2 answers
95 views

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

0 votes
1 answer
40 views

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

0 votes
1 answer
32 views

ACL2 Prove that the product of two positive numbers is positive

2 votes
1 answer
62 views

Checking if a goal is *definitely wrong* by testing it against random examples in Coq

1 vote
1 answer
42 views

Applying an axiom from a class in a proof

1 vote
1 answer
86 views

Trying to use 'Equations'

0 votes
2 answers
55 views

Coq can you enter a tactic context inside of a `Fixpoint` definition?

1 vote
2 answers
65 views

Dependent equality in Coq

Browse more Questions