last day (65 days later) » 

Wheat Witch
Wheat Witch
12:41
Hello!
user
user
Nice name :P
Might want to add leanprover-community.github.io to the room description?
Wheat Witch
Wheat Witch
room topic changed to The Lean-to: A room for discussing Lean the Language of the Month for October 2021. leanprover-community.github.io (no tags)
user
user
12:59
The natural number game is a really nice tutorial
Wheat Witch
Wheat Witch
Yeah. It's pretty fun.
Huỳnh Trần Khanh
Huỳnh Trần Khanh
Hello, Khanh here.
Wheat Witch
Wheat Witch
Hello.
Huỳnh Trần Khanh
Huỳnh Trần Khanh
Would you like to learn some Lean 👉👈 Which version would you like to learn, Lean 3 or Lean 4?
I don't speak Lean 4 though but it's more well suited as a programming language.
Lean 3, however, is more mature, it has more learning resources but its execution speed is somewhat slow.
Wheat Witch
Wheat Witch
I'm going through the natural number game first.
Huỳnh Trần Khanh
Huỳnh Trần Khanh
13:07
It's in Lean 3.
Wheat Witch
Wheat Witch
Yeah. But I may use Lean 4 later. I'm just getting a feel first.
user
user
@HuỳnhTrầnKhanh Are there significant differences in the syntax or concepts?
Huỳnh Trần Khanh
Huỳnh Trần Khanh
@user The axiomatic foundation is the same, however, the two versions are drastically different. I have absolutely no idea how to use Lean 4.
Also, mathlib isn't available for Lean 4 yet. So it will be a lot more painful to use Lean 4.
user
user
Oh, interesting
 
4 hours later…
Huỳnh Trần Khanh
Huỳnh Trần Khanh
16:51
Could Lean be used in proof-golf challenges? Or would that be problematic?
Could we force answers to use certain theorem proving languages only, such as Coq, Agda or Lean?
Because otherwise someone would make a homebrew theorem prover and write a proof that's based on unsound foundations.
Should I make a meta post to discuss this? Or maybe someone in here should make one, as I won't be available tomorrow.
 
1 hour later…
user
user
18:09
@HuỳnhTrầnKhanh I don't think that's how proof-golf works
This challenge introduces its own axioms (which are sound)

  last day (65 days later) »