<commit_before>---
layout: archive
title: "Links"
date:
modified:
excerpt:
image:
  feature:
  teaser:
  thumb:
ads: false
---

## Chat Room

- A public chat room dedicated to Lean is open on [Zulip](https://leanprover.zulipchat.com/).

## Twitter

- The official [Lean twitter](https://twitter.com/leanprover) account.

- [Kevin's Buzzard twitter](https://twitter.com/XenaProject) about Lean.

## Popular science articles about Lean

- [Wired article](https://www.wired.com/story/the-effort-to-build-the-mathematical-library-of-the-future/) about the Lean mathematical library.

- [Nature's article](https://media.nature.com/original/magazine-assets/d41586-021-01627-2/d41586-021-01627-2.pdf) about [<NAME>](https://en.wikipedia.org/wiki/Peter_Scholze)'s (Fields Medal in 2018) project formalized in Lean.

- [<NAME>'s article](https://bigthink.com/technology-innovation/artificial-intelligence-replace-mathematicians) mentioning Scholze's result and Lean.

- [Proof Assistant Makes Jump to Big League Math](https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/), Quanta article about Scholze's result and Lean.

- [Quanta article](https://www.quantamagazine.org/at-the-international-mathematical-olympiad-artificial-intelligence-prepares-to-go-for-the-gold-20200921/) about the IMO grand challenge.

- Lean has been mentioned in Quanta's The Year in Math and Computer Science two years in a row: [2020](https://www.quantamagazine.org/the-year-in-math-and-computer-science-20201223/) and [2021](https://www.quantamagazine.org/the-year-in-math-and-computer-science-20211223/).

## Videos<commit_msg>link to Lean Nightlies<commit_after>---
layout: archive
title: "Links"
date:
modified:
excerpt:
image:
  feature:
  teaser:
  thumb:
ads: false
---

## Chat Room

- A public chat room dedicated to Lean is open on [Zulip](https://leanprover.zulipchat.com/).

## Twitter

- The official [Lean twitter](https://twitter.com/leanprover) account.

- [Lean Nightlies](https://twitter.com/lean4_nightly) tweets release notes from [https://github.com/leanprover/lean4-nightly/releases](https://github.com/leanprover/lean4-nightly/releases)

- [Kevin's Buzzard twitter](https://twitter.com/XenaProject) about Lean.

## Popular science articles about Lean

- [Wired article](https://www.wired.com/story/the-effort-to-build-the-mathematical-library-of-the-future/) about the Lean mathematical library.

- [Nature's article](https://media.nature.com/original/magazine-assets/d41586-021-01627-2/d41586-021-01627-2.pdf) about [Peter Scholze](https://en.wikipedia.org/wiki/Peter_Scholze)'s (Fields Medal in 2018) project formalized in Lean.

- [<NAME>'s article](https://bigthink.com/technology-innovation/artificial-intelligence-replace-mathematicians) mentioning Scholze's result and Lean.

- [Proof Assistant Makes Jump to Big League Math](https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/), Quanta article about Scholze's result and Lean.

- [Quanta article](https://www.quantamagazine.org/at-the-international-mathematical-olympiad-artificial-intelligence-prepares-to-go-for-the-gold-20200921/) about the IMO grand challenge.

- Lean has been mentioned in Quanta's The Year in Math and Computer Science two years in a row: [2020](https://www.quantamagazine.org/the-year-in-math-and-computer-science-20201223/) and [2021](https://www.quantamagazine.org/the-year-in-math-and-computer-science-20211223/).

## Videos
{'fraction_non_alphanumeric': 0.14310344827586208, 'fraction_numerical': 0.04224137931034483, 'mean_word_length': 4.734761120263592, 'pattern_counts': {'":': 0, '<': 6, '<?xml version=': 0, '>': 6, 'https://': 25, 'lorem ipsum': 0, 'www.': 10, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6667680', 'n_tokens_mistral': 1306, 'n_tokens_neox': 1159, 'n_words': 236}