Explore our questions

0 votes
0 answers
13 views

Given some proposition in Lean 4, how do we state a theorem saying that we want that property to hold a number of times?

0 votes
0 answers
35 views

Can proof assistants reflect the informal notion of a “theory” as the formally logical notion of a “theory”?

1 vote
1 answer
59 views

How do I explicitly see the propositional or logical constructors in Lean 4?

1 vote
1 answer
23 views

Isabelle warning explanation

25 votes
2 answers
708 views

What is Artin gluing, and how is it useful in proving meta-theoretic properties?

2 votes
2 answers
152 views

Binding variables to terms involving later variables

0 votes
2 answers
39 views

Why can't Lean4 evaluate my function despite it being defined, Error: compiler IR check failed at '_eval', error: unknown declaration 'g'?

1 vote
1 answer
47 views

Where does one find the keyword documentation for Lean4?

2 votes
2 answers
128 views

How exactly solved metas "revisited" in an efficient dependent type checker?

0 votes
1 answer
21 views

How do I construct a concrete real number in lean without errors? failed to synthesize instance OfScientific ℝ

1 vote
2 answers
88 views

How does one create a lean project and have mathlib import work when not creating the lean project at the $HOME directory?

6 votes
1 answer
200 views

What are the principal differences between Agda's core type theory and Coq's?

1 vote
1 answer
38 views

Using coIH as an argument to the transitivity of Bisimilarity (cofix and pcofix)

1 vote
1 answer
41 views

How do I write bitwise logic in lean4 with mathlib?

Browse more Questions