Add Lean4

[CrSb0001]

This issue is related to #263, however I decided to re-raise it considering the original issue is just over 2 years old, and because there doesn't seem to have been any discussion on it.

• Name: Lean 4
• Website: https://leanprover.github.io/
• Language Version:
  • Most recent release: v4.25.0-rc2
  • Most recent stable releases: v4.24.0, v4.23.0
• Comments: From its documentation on Github (and also https://lean-lang.org/), Lean 4 is an open source proof assistant and programming language that is meant to enable maintainable and formally verified code. Its metaprogramming capabilities enable users to extend the language as necessary.

---

• Test Frameworks:

  • For functional programming: LTest is the only one I'm aware of (since there isn't a built-in test framework in Lean 4), although at the moment it doesn't seem to be very fleshed out.
    However, if needed, I'm pretty sure I could throw together a fleshed out test framework from scratch by March of next year.
    
    
  • For theorems: I'm sure a test framework wouldn't be needed in this case (considering there is none for Lean 3)

• How to install: See here for VSCode instructions, although installation should be possible through Atom using a similar method.

• How to compile/run: Should be the same as or at least similar to Lean 3 (although I don't really know).

• Any comments: Configuration dependencies for a project require either a lakefile.lean or lakefile.toml file (I've seen both).

---

Closing notes:

• On extensibility to more general programming challenges: I have been able to translate some of my own kata solutions to Lean 4 with somewhat similar (although slightly worse) performance overall, while also being able to verify that the data types needed to solve each problem are available natively.

  • Some of the (more notable) kata of which I have been able to translate my solution into Lean 4 include:

    • The Hashtag Generator (5 kyu)
    • Bitwise Sum (4 kyu)
    • Lowest base system (4 kyu)
    • BasE91 encoding & decoding (4 kyu)
    • The fusc function -- Part 2 (4 kyu)
    • Differentiate a polynomial (4 kyu)²
    • Memoized Log Cutting (4 kyu)
    • Sum Strings as Numbers (4 kyu)¹
    • Matrix Determinant (4 kyu)
    • SKRZAT!!! (4 kyu)¹
    • Rail Fence Cipher: Encoding and Decoding (3 kyu)²
    • Last digit of a huge number (3 kyu)¹
    • Fabergé Easter Eggs crush test (3 kyu)
    • The Millionth Fibonacci Kata (3 kyu)¹ ³
    • Power tower modulo n (2 kyu)
    • Faberge easter eggs crush test [linear] (1 kyu)
    • BECOME IMMORTAL (1 kyu)

  • The kata which I previously solved and am currently attempting to write a solution for in Lean 4:

    • Gould's Sequence (7 kyu)
    • 4 By 4 Skyscrapers (4 kyu)
    • Battleship Field Validator (3 kyu)
    • Fastest Code: Equal to 24 (2 kyu)
    • 6 By 6 Skyscrapers (2 kyu)
    • 7 By 7 Skyscrapers (1 kyu)

• External Dependencies Requested:

  • Mathlib4 (leanprover-community)
  • Ctypes (alexf91)

---

^{¹The Lean 4 translation can still be optimized, although not much more optimization should be needed to handle larger test cases.
²The Lean 4 translation needs to be more optimized before tagging with ¹.
³Translated using solutions I've used in the past, not the one used to solve the kata.}

👍 reaction might help to get this request prioritized.