Mirror
/
zulip
mirror of https://github.com/zulip/zulip.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

portico: Make minor fixes in Lean case study.

This commit is contained in:
Alya Abbott 2022-01-19 12:01:56 -08:00 committed by Tim Abbott
parent ce5153adee
commit e7e422ff13
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
templates/zerver/for/lean-case-study.md
View File

@ -9,8 +9,8 @@ project](https://leanprover-community.github.io/) to develop the [Lean theorem
prover](https://leanprover.github.io/) mathematics library.
The Lean prover project was [featured in Nature magazine in June
2021](https://www.nature.com/articles/d41586-021-01627-2), when an automated
proof system was successfully used to [verify a result at the cutting edge of
2021](https://www.nature.com/articles/d41586-021-01627-2), when the interactive
theorem prover was successfully used to [verify a result at the cutting edge of
mathematical
research](https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/).
This accomplishment was the result of a deep multi-month collaboration between
@ -54,7 +54,7 @@ mathematics is taught.
## Unified library of mathematics developed by a diverse community
Lean is an interactive theorem-prover and a programming language. Like C++ or
Lean is an interactive theorem prover and a programming language. Like C++ or
Python, it would be impossible to use in practice without a library of
pre-defined components — imagine writing a function from scratch every time you
need to sort a list! The functions that make it possible to “program” in Lean