Zulip Chat Archive

Stream: new members

Topic: Software Foundations


view this post on Zulip Phiroc (Mar 18 2021 at 12:49):

Hello,
Has anyone here worked through the exercises in the Software Foundations Book, in Lean 3 or 4? If not, would anyone like to collaborate on finding solutions? I am using Lean 4.

view this post on Zulip Kevin Buzzard (Mar 18 2021 at 13:08):

When I was learning Lean I went through most of the first SF book and ported solutions to Lean 3 (and didn't keep them); I can certainly say that it taught me a lot (I didn't know anything about theorem provers at the time and SF seemed to be a good teaching resource). I am not going to go through this stuff again myself but I would definitely say that if there are beginners out there who want to read a good teaching textbook written in a language close to Lean then this might be a great opportunity.

view this post on Zulip Julian Berman (Mar 18 2021 at 16:24):

@Phiroc my attention span is always scattered, but if you're going through that in some public place (e.g. GitHub) I'd be interested in following the progress and perhaps contributing in ad hoc ways, I've had software foundations somewhere on my list to read. The majority of my interest in Lean is to get closer to some math moreso than formal validation more generally, so I don't know that I'll be super helpful on an ongoing basis but yeah definitely keen to learn.

view this post on Zulip Phiroc (Mar 18 2021 at 19:32):

Julian Berman said:

Phiroc my attention span is always scattered, but if you're going through that in some public place (e.g. GitHub) I'd be interested in following the progress and perhaps contributing in ad hoc ways, I've had software foundations somewhere on my list to read. The majority of my interest in Lean is to get closer to some math moreso than formal validation more generally, so I don't know that I'll be super helpful on an ongoing basis but yeah definitely keen to learn.

Hi Julian, I've just created a private Software-Foundations-In-Lean project on GitHub. Once I have made sufficient progress, I'll make it public so that anyone who wants to can contribute.

view this post on Zulip Shing Tak Lam (Mar 18 2021 at 19:42):

Phiroc said:

Julian Berman said:

Phiroc my attention span is always scattered, but if you're going through that in some public place (e.g. GitHub) I'd be interested in following the progress and perhaps contributing in ad hoc ways, I've had software foundations somewhere on my list to read. The majority of my interest in Lean is to get closer to some math moreso than formal validation more generally, so I don't know that I'll be super helpful on an ongoing basis but yeah definitely keen to learn.

Hi Julian, I've just created a private Software-Foundations-In-Lean project on GitHub. Once I have made sufficient progress, I'll make it public so that anyone who wants to can contribute.

By the way, the authors of SF ask that the solutions to exercises are not made public, and although SF is written in Coq, Lean is similar enough that it might be transferrable. I don't think they would mind if the repo contains only the exercises.

view this post on Zulip Guilherme Espada (Mar 18 2021 at 21:31):

Why do they ask for the solutions not to be made public? Seems a bit weird for self-learning

view this post on Zulip Scott Morrison (Mar 18 2021 at 22:07):

Presumably because it makes it hard to use the problems as homework assignments for students.

view this post on Zulip Phiroc (Mar 19 2021 at 07:16):

I’ll therefore translate the code examples and implementations to Lean 4, and leave out the answers, or answer attempts, to the exercises . It’s a pity though, because I am having a hard time finding answers to some exercises, in idiomatic Lean.

view this post on Zulip Iocta (Mar 19 2021 at 08:46):

(deleted)

view this post on Zulip Alex J. Best (Mar 19 2021 at 21:58):

I guess there's nothing wrong with asking for idiomatic lean ways of doing specific questions here, just not writing an easy to find least of solutions to every exercise would be bad for instructors of classes


Last updated: May 06 2021 at 20:13 UTC