Hacker News Reader

Hacker News

Comment by brcmthrowaway | Hacker News Reader

Parent Full thread

brcmthrowaway

What is Lean FRO?

View on HN

https://lean-fro.org/about/

Yeah that really doesn’t help.

FWIW, not having done a proof since about 1982, it doesn't help me either.

we aim to tackle the challenges of scalability, usability, and proof automation in the Lean proof assistant https://lean-lang.org/

Yep. Truly a mystery.

~~Nice addition of a link that doesn't exist in the actual "quoted" source. If it did exist it would certainly be helpful though, so thanks for adding it I guess.~~

EDIT: Apparently their website design is just so poor their clickable links are identical to the non-clickable plain text. That link is a clickable word if you completely guess you can click on some of the apparent plain text.

Lean is a currently-niche programming language / proof-assistant. A proof assistant is basically a tool to construct mathematical proofs, which verifies that the proofs are correct like how a compiler verifies types in your programs.

IIUC a regular programming language with a certain set of restrictions already duals as a proof-assistant as discovered by Curry & Howard. By restrictions, I mean something like how Rust forces you to follow certain rules compared to Java.

Background about the organization: https://en.m.wikipedia.org/wiki/Convergent_Research

Their proof assistant / programming language: https://en.m.wikipedia.org/wiki/Lean_(proof_assistant)

https://lean-lang.org/lean4/doc/

There are a lot of broken links in the docs. Like most of the feature links.

There's a completely new language reference in the process of being written: https://lean-lang.org/doc/reference/latest/ (by David Thrane Christiansen, co-author of The Little Typer, and Lean FRO member)

Some links here seem to be broken at the moment — and David's currently on vacation so they likely won't be fixed until January — but if you see for example https://lean-lang.org/basic-types/strings/ it's supposed to be https://lean-lang.org/doc/reference/latest/basic-types/strin...

That answers the Lean part, FRO stands for Focused Research Organization

That doesn't say much.. Research on what? It looks like Lean is a programming language but everything else is pretty abstract to me.

"we aim to tackle the challenges of scalability, usability, and proof (Mathematics) automation in the Lean proof assistant."

Reply on news.ycombinator.com