-
Notifications
You must be signed in to change notification settings - Fork 220
List of Lean Kata to Update
Donald Sebastian Leung edited this page Oct 9, 2020
·
62 revisions
The following kata are not compatible with Lean v3.20.0 with mathlib da66bb81bf0466335bae82077f0c335dfe53aeb3
:
- (5^5^5^5^5-1)/(5^5^(5^5^5-1)-1) isn't prime
- Easy Fermat
- Find the number of bits and the bits with proof
- Generalised Pell x^2-37y^2=3
- If a^b + 1 is prime, then a is even
- If a^b + 1 is prime, then b is a power of two
- If N divides 2^N - 1, then N is zero or one
- Index 2 subgroup is normal
- Limit of the arithmetic mean
- Order-preserving bijection from rationals to non-zero rationals
- Program Verification #4: Exponentiation by squaring
- Prove that a ^ 4 - b ^ 4 = (a - b) * (a + b) * (a ^ 2 + b ^ 2), using nats
- Prove that this sequence contains only integers
- Squared triangular numbers
- Squareful segments
- Verified Horner's method