5 ms·

What is Lean FRO?

by brcmthrowaway 2y ago

What is Lean FRO?

cwzwarich 2y ago
https://lean-fro.org/about/ https://lean-fro.org/about/
- hinkley 2y ago
  Yeah that really doesn’t help.
  - lambdas 2y ago
    we aim to tackle the challenges of scalability, usability, and proof automation in the Lean proof assistant https://lean-lang.org/ https://lean-lang.org/ Yep. Truly a mystery.
    - aaravchen 2y ago
      ~~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.
  - lproven 2y ago
    FWIW, not having done a proof since about 1982, it doesn't help me either.
threeseed 2y ago
https://lean-lang.org/lean4/doc/ https://lean-lang.org/lean4/doc/
- croemer 2y ago
  That answers the Lean part, FRO stands for Focused Research Organization
  - swat535 2y ago
    That doesn't say much.. Research on what? It looks like Lean is a programming language but everything else is pretty abstract to me.
- jemmyw 2y ago
  There are a lot of broken links in the docs. Like most of the feature links.
  - kmill 2y ago
    There's a completely new language reference in the process of being written: https://lean-lang.org/doc/reference/latest/ 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/ https://lean-lang.org/basic-types/strings/ it's supposed to be https://lean-lang.org/doc/reference/latest/basic-types/strings/ https://lean-lang.org/doc/reference/latest/basic-types/strin...
bagels 2y ago
"we aim to tackle the challenges of scalability, usability, and proof (Mathematics) automation in the Lean proof assistant."
thih9 2y ago
Background about the organization: https://en.m.wikipedia.org/wiki/Convergent_Research https://en.m.wikipedia.org/wiki/Convergent_Research Their proof assistant / programming language: https://en.m.wikipedia.org/wiki/Lean_(proof_assistant) https://en.m.wikipedia.org/wiki/Lean_(proof_assistant)
yairchu 2y ago
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.

What is Lean FRO?

cwzwarich 2y ago

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

hinkley 2y ago
Yeah that really doesn’t help.
- lambdas 2y ago
  we aim to tackle the challenges of scalability, usability, and proof automation in the Lean proof assistant https://lean-lang.org/ https://lean-lang.org/ Yep. Truly a mystery.
  - aaravchen 2y ago
    ~~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.
- lproven 2y ago
  FWIW, not having done a proof since about 1982, it doesn't help me either.

threeseed 2y ago

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

croemer 2y ago
That answers the Lean part, FRO stands for Focused Research Organization
- swat535 2y ago
  That doesn't say much.. Research on what? It looks like Lean is a programming language but everything else is pretty abstract to me.
jemmyw 2y ago
There are a lot of broken links in the docs. Like most of the feature links.
- kmill 2y ago
  There's a completely new language reference in the process of being written: https://lean-lang.org/doc/reference/latest/ 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/ https://lean-lang.org/basic-types/strings/ it's supposed to be https://lean-lang.org/doc/reference/latest/basic-types/strings/ https://lean-lang.org/doc/reference/latest/basic-types/strin...

bagels 2y ago

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

thih9 2y ago

Background about the organization: https://en.m.wikipedia.org/wiki/Convergent_Research https://en.m.wikipedia.org/wiki/Convergent_Research Their proof assistant / programming language: https://en.m.wikipedia.org/wiki/Lean_(proof_assistant) https://en.m.wikipedia.org/wiki/Lean_(proof_assistant)

yairchu 2y ago

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.