Thank you
Learning Lean: Part 1
11–18 of 18 posts
Re: Learning Lean: Part 1
#12It's interesting to see the notes of someone tackling lean who's primary occupation is SWE but has a strong background in mathematics.
Lean is great, but if someone's primary interest is SWE, I think there are better choices. The Lean community is primarily focused on formalizing mathematics right now. This might change in the future. Lean is nice to learn theorem proving, but once you learn the basics, you'll hit a roadblock when trying to move to software verification applications. For SWE, the most mature option is probably Isabelle. It's also a…
If verification is the goal, but you don't want to learn theorem proving yet, Dafny is really approachable and practical [1]. F* is also worth considering as a proof-oriented alternative to Isabelle that is focused on software verification [2]. Why3, Rocq and Agda are other obvious contenders.
Re: Learning Lean: Part 1
#13It's interesting to see the notes of someone tackling lean who's primary occupation is SWE but has a strong background in mathematics.
Lean is great, but if someone's primary interest is SWE, I think there are better choices. The Lean community is primarily focused on formalizing mathematics right now. This might change in the future. Lean is nice to learn theorem proving, but once you learn the basics, you'll hit a roadblock when trying to move to software verification applications. For SWE, the most mature option is probably Isabelle. It's also a…
The future is now. The recent couple of Lean releases have leaned more on software verification, I believe in part due to Amazon hiring a number of the core devs.
Re: Learning Lean: Part 1
#14I never hijack non-ai threads to talk about AI, but can anybody share their experience using LLMs to code in Coq, Lean, etc.
I’ve never used them first hand, but crackpots sure do love claiming to solve Riemann hypothesis, P vs NP, Collatz conjecture etc and then peddle out some huge slop. My experience has solely been curiously following what the LLM’s have been generating. You have to be very, VERY careful. With how predisposed they are to helping, they’ll turn to “dishonesty” rather than just shut down and refuse. What I tend to see is…
> introducing an error or two in formal proof systems often means you’re getting exponentially further away from solving your problem
I wish people understood that this is pretty much true of software building as well.
Re: Learning Lean: Part 1
#15i am a mathematician wanna-be. I have an undergrad honours degree in maths. As a retirement or pre-retirement project, I want to learn LEAN and contribute to it either via development or via developing the Mathlib or both!
Pointers welcome. As long as they are not null. Btw, I am also interested in compilers.
Re: Learning Lean: Part 1
#16I never hijack non-ai threads to talk about AI, but can anybody share their experience using LLMs to code in Coq, Lean, etc.
I’ve never used them first hand, but crackpots sure do love claiming to solve Riemann hypothesis, P vs NP, Collatz conjecture etc and then peddle out some huge slop. My experience has solely been curiously following what the LLM’s have been generating. You have to be very, VERY careful. With how predisposed they are to helping, they’ll turn to “dishonesty” rather than just shut down and refuse. What I tend to see is…
>So even when it compiles, you’ve got the burden of verifying everything is above board which is a pretty huge task.
Is this true?
e.g. the Riemann hypothesis is in mathlib:
def RiemannHypothesis : Prop :=
∀ (s : ℂ) (_ : riemannZeta s = 0) (_ : ¬∃ n : ℕ, s = -2 * (n + 1)) (_ : s ≠ 1), s.re = 1 / 2
Re: Learning Lean: Part 1
#17Earlier quoted context omitted.
I’ve never used them first hand, but crackpots sure do love claiming to solve Riemann hypothesis, P vs NP, Collatz conjecture etc and then peddle out some huge slop. My experience has solely been curiously following what the LLM’s have been generating. You have to be very, VERY careful. With how predisposed they are to helping, they’ll turn to “dishonesty” rather than just shut down and refuse. What I tend to see is…
> So even when it compiles, you’ve got the burden of verifying everything is above board which is a pretty huge task. Is this true? e.g. the Riemann hypothesis is in mathlib: def RiemannHypothesis : Prop := ∀ (s : ℂ) (_ : riemannZeta s = 0) (_ : ¬∃ n : ℕ, s = -2 * (n + 1)) (_ : s ≠ 1), s.re = 1 / 2 If I construct a term of this type without going via one of the (fairly obvious) soundness holes or a compiler bug, it's…
Sorry, I mean verify the semantics of what the LLM has generated is exactly what you were asking for.
Re: Learning Lean: Part 1
#18Earlier quoted context omitted.
> So even when it compiles, you’ve got the burden of verifying everything is above board which is a pretty huge task. Is this true? e.g. the Riemann hypothesis is in mathlib: def RiemannHypothesis : Prop := ∀ (s : ℂ) (_ : riemannZeta s = 0) (_ : ¬∃ n : ℕ, s = -2 * (n + 1)) (_ : s ≠ 1), s.re = 1 / 2 If I construct a term of this type without going via one of the (fairly obvious) soundness holes or a compiler bug, it's…
Sorry, I mean verify the semantics of what the LLM has generated is exactly what you were asking for.
I don't understand that. If it has a correct statement of the theorem and no `believe-me`s or whatever, it should be correct.