From df26fddf394e8ede515caf77b269e9283ef02501 Mon Sep 17 00:00:00 2001 From: leanprover-community-bot Date: Wed, 18 Sep 2024 00:13:43 +0000 Subject: [PATCH] deploy site from 8184b19cac8c626b33935b362fb19c0856c87789 --- docs/2024/index.html | 3 + docs/archive.html | 2 +- docs/authors/adam-topaz.xml | 2 +- docs/authors/anne-baanen.xml | 2 +- docs/authors/chris-birkbeck.xml | 2 +- docs/authors/david-chanin.xml | 2 +- docs/authors/emily-riehl.xml | 3 + docs/authors/emily-riehl/index.html | 65 +++++++ docs/authors/frederic-dupuis.xml | 2 +- docs/authors/heather-macbeth.xml | 2 +- docs/authors/index.html | 1 + docs/authors/jana-goken.xml | 2 +- docs/authors/jeremy-avigad.xml | 2 +- docs/authors/johan-commelin.xml | 2 +- docs/authors/kevin-buzzard.xml | 2 +- docs/authors/kexing-ying.xml | 2 +- docs/authors/mathlib-community.xml | 2 +- docs/authors/patrick-massot.xml | 2 +- docs/authors/riccardo-brasca.xml | 2 +- docs/authors/robert-y-lewis.xml | 2 +- docs/authors/scott-morrison.xml | 2 +- docs/authors/the-lean-prover-community.xml | 2 +- docs/authors/yury-kudryashov.xml | 2 +- docs/categories/-cosmos.xml | 3 + docs/categories/-cosmos/index.html | 66 +++++++ docs/categories/backstage.xml | 2 +- docs/categories/cat_announcement.xml | 2 +- docs/categories/cat_announcements.xml | 2 +- docs/categories/cat_community-projects.xml | 2 +- docs/categories/cat_interviews.xml | 2 +- docs/categories/cat_mathport.xml | 2 +- docs/categories/cat_meeting-report.xml | 2 +- docs/categories/cat_month-in-mathlib.xml | 2 +- docs/categories/cat_new-in-mathlib.xml | 2 +- docs/categories/cat_overview.xml | 2 +- docs/categories/cat_papers.xml | 2 +- docs/categories/cat_project-announcement.xml | 3 +- .../cat_project-announcement/index.html | 3 + docs/categories/index.html | 1 + docs/index-4.html | 19 +- docs/index.html | 38 ++-- .../infinity-cosmos-announcement/index.html | 116 +++++++++++ .../infinity-cosmos-announcement/index.md | 38 ++++ .../2024/month-in-mathlib-may-2024/index.html | 4 + docs/rss.xml | 6 +- docs/sitemap.xml | 184 ++++++++++-------- docs/sitemapindex.xml | 72 ++++--- 47 files changed, 513 insertions(+), 172 deletions(-) create mode 100644 docs/authors/emily-riehl.xml create mode 100644 docs/authors/emily-riehl/index.html create mode 100644 docs/categories/-cosmos.xml create mode 100644 docs/categories/-cosmos/index.html create mode 100644 docs/posts/infinity-cosmos-announcement/index.html create mode 100644 docs/posts/infinity-cosmos-announcement/index.md diff --git a/docs/2024/index.html b/docs/2024/index.html index c40a3142..353f86fd 100644 --- a/docs/2024/index.html +++ b/docs/2024/index.html @@ -43,6 +43,9 @@

Posts for year 2024

  • +Announcing the ∞-Cosmos Project +
    • +
  • This month in Mathlib (May 2024)
  • diff --git a/docs/archive.html b/docs/archive.html index 2fe14c4f..b5b5d25a 100644 --- a/docs/archive.html +++ b/docs/archive.html @@ -44,7 +44,7 @@
    • 2024 - (2) + (3)
    • 2023 diff --git a/docs/authors/adam-topaz.xml b/docs/authors/adam-topaz.xml index 3842bf54..3b00d800 100644 --- a/docs/authors/adam-topaz.xml +++ b/docs/authors/adam-topaz.xml @@ -1,5 +1,5 @@ -Lean community blog (Posts by Adam Topaz)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:21 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssDefinitions in the liquid tensor experimenthttps://leanprover-community.github.io/blog/posts/lte-examples/Adam Topaz<div><p>A few weeks ago, we announced the <a href="https://leanprover-community.github.io/blog/posts/lte-final/">completion of the liquid tensor experiment</a> (<strong>LTE</strong> for short). +Lean community blog (Posts by Adam Topaz)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssDefinitions in the liquid tensor experimenthttps://leanprover-community.github.io/blog/posts/lte-examples/Adam Topaz<div><p>A few weeks ago, we announced the <a href="https://leanprover-community.github.io/blog/posts/lte-final/">completion of the liquid tensor experiment</a> (<strong>LTE</strong> for short). What this means is that we stated and (completely) proved the following result in Lean:</p> <pre class="code literal-block"><span class="kd">variables</span> <span class="o">(</span><span class="n">p'</span> <span class="n">p</span> <span class="o">:</span> <span class="n">ℝ</span><span class="bp">≥</span><span class="mi">0</span><span class="o">)</span> <span class="o">[</span><span class="n">fact</span> <span class="o">(</span><span class="mi">0</span> <span class="bp">&lt;</span> <span class="n">p'</span><span class="o">)]</span> <span class="o">[</span><span class="n">fact</span> <span class="o">(</span><span class="n">p'</span> <span class="bp">&lt;</span> <span class="n">p</span><span class="o">)]</span> <span class="o">[</span><span class="n">fact</span> <span class="o">(</span><span class="n">p</span> <span class="bp">≤</span> <span class="mi">1</span><span class="o">)]</span> diff --git a/docs/authors/anne-baanen.xml b/docs/authors/anne-baanen.xml index afc508a3..97697221 100644 --- a/docs/authors/anne-baanen.xml +++ b/docs/authors/anne-baanen.xml @@ -1,5 +1,5 @@ -Lean community blog (Posts by Anne Baanen)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:21 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssDedekind domains and class number in Leanhttps://leanprover-community.github.io/blog/posts/dedekind-domains-and-class-number-in-lean/Anne Baanen<div><p>Pull request <a href="https://github.com/leanprover-community/mathlib/pull/9071">#9701</a> marks the completion of a string of additions to mathlib centered around formalizing Dedekind domains and class groups of global fields (those words will be explained below). Previous PRs had shown that nonzero ideals of a Dedekind domain factor uniquely into prime ideals, and had defined class groups in some generality. The main result in this PR is the finiteness of the class group of a global field (and in particular of the ring of integers of a number field). +Lean community blog (Posts by Anne Baanen)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssDedekind domains and class number in Leanhttps://leanprover-community.github.io/blog/posts/dedekind-domains-and-class-number-in-lean/Anne Baanen<div><p>Pull request <a href="https://github.com/leanprover-community/mathlib/pull/9071">#9701</a> marks the completion of a string of additions to mathlib centered around formalizing Dedekind domains and class groups of global fields (those words will be explained below). Previous PRs had shown that nonzero ideals of a Dedekind domain factor uniquely into prime ideals, and had defined class groups in some generality. The main result in this PR is the finiteness of the class group of a global field (and in particular of the ring of integers of a number field). Formalizing these subjects has been one of my long-term goals for mathlib, and as far as we are aware, Lean is the first system in which this level of algebraic number theory is available. These formalizations have been joint work: diff --git a/docs/authors/chris-birkbeck.xml b/docs/authors/chris-birkbeck.xml index 20916d6c..84d4cc9e 100644 --- a/docs/authors/chris-birkbeck.xml +++ b/docs/authors/chris-birkbeck.xml @@ -1,3 +1,3 @@ -Lean community blog (Posts by Chris Birkbeck)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:22 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssModular formshttps://leanprover-community.github.io/blog/posts/modular-forms/Chris Birkbeck<div><p>In <a href="https://github.com/leanprover-community/mathlib/pull/13250">PR# 13250</a> we define modular forms and cusp forms, and prove that they form complex vector spaces. These are analytic functions of number theoretic interest with strong links to geometry, representation theory and analysis. Most famously they are a key ingredient in the proof of Fermat's Last Theorem. In this post we discuss the formalization process, motivate some design choices and map out some future work.</p> +Lean community blog (Posts by Chris Birkbeck)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssModular formshttps://leanprover-community.github.io/blog/posts/modular-forms/Chris Birkbeck<div><p>In <a href="https://github.com/leanprover-community/mathlib/pull/13250">PR# 13250</a> we define modular forms and cusp forms, and prove that they form complex vector spaces. These are analytic functions of number theoretic interest with strong links to geometry, representation theory and analysis. Most famously they are a key ingredient in the proof of Fermat's Last Theorem. In this post we discuss the formalization process, motivate some design choices and map out some future work.</p> <p><a href="https://leanprover-community.github.io/blog/posts/modular-forms/">Read more…</a> (7 min remaining to read)</p></div>https://leanprover-community.github.io/blog/posts/modular-forms/Wed, 21 Dec 2022 11:41:21 GMT \ No newline at end of file diff --git a/docs/authors/david-chanin.xml b/docs/authors/david-chanin.xml index cbb05d97..4db22ed1 100644 --- a/docs/authors/david-chanin.xml +++ b/docs/authors/david-chanin.xml @@ -1,4 +1,4 @@ -Lean community blog (Posts by David Chanin)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:21 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssIntroducing Mathlib Changeloghttps://leanprover-community.github.io/blog/posts/mathlib-changelog/David Chanin<div><p><img alt="mathlib-changelog sample page" src="https://leanprover-community.github.io/blog/images/changelog_lemma.png"></p> +Lean community blog (Posts by David Chanin)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssIntroducing Mathlib Changeloghttps://leanprover-community.github.io/blog/posts/mathlib-changelog/David Chanin<div><p><img alt="mathlib-changelog sample page" src="https://leanprover-community.github.io/blog/images/changelog_lemma.png"></p> <p>Tldr; check out <a href="https://mathlib-changelog.org">mathlib-changelog.org</a> to explore the historical changes to mathlib, and find out what happened to that lemma you were using.</p> <p><a href="https://leanprover-community.github.io/blog/posts/mathlib-changelog/">Read more…</a> (3 min remaining to read)</p></div>https://leanprover-community.github.io/blog/posts/mathlib-changelog/Thu, 28 Jul 2022 07:35:23 GMT \ No newline at end of file diff --git a/docs/authors/emily-riehl.xml b/docs/authors/emily-riehl.xml new file mode 100644 index 00000000..1944b22c --- /dev/null +++ b/docs/authors/emily-riehl.xml @@ -0,0 +1,3 @@ + +Lean community blog (Posts by Emily Riehl)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssAnnouncing the ∞-Cosmos Projecthttps://leanprover-community.github.io/blog/posts/infinity-cosmos-announcement/Emily Riehl<div><p><a href="https://github.com/emilyriehl">Emily Riehl</a> introduces the <a href="https://github.com/emilyriehl/infinity-cosmos">∞-Cosmos Project</a>.</p> +<p><a href="https://leanprover-community.github.io/blog/posts/infinity-cosmos-announcement/">Read more…</a> (2 min remaining to read)</p></div>∞-Cosmoshttps://leanprover-community.github.io/blog/posts/infinity-cosmos-announcement/Tue, 17 Sep 2024 18:00:00 GMT \ No newline at end of file diff --git a/docs/authors/emily-riehl/index.html b/docs/authors/emily-riehl/index.html new file mode 100644 index 00000000..b65ea740 --- /dev/null +++ b/docs/authors/emily-riehl/index.html @@ -0,0 +1,65 @@ + + + + + +Posts by Emily Riehl | Lean community blog + + + + + + + + + + + + + + + + + Skip to main content +
      +

      Contents © 2024 The Lean prover community - Powered by Nikola

      + +
      +
      + + + + + + diff --git a/docs/authors/frederic-dupuis.xml b/docs/authors/frederic-dupuis.xml index 9e4de13d..352fe713 100644 --- a/docs/authors/frederic-dupuis.xml +++ b/docs/authors/frederic-dupuis.xml @@ -1,3 +1,3 @@ -Lean community blog (Posts by Frédéric Dupuis)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:21 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssSemilinear mapshttps://leanprover-community.github.io/blog/posts/semilinear-maps/Frédéric Dupuis<div><p>Since linear maps appear everywhere in mathematics, it comes as no surprise that they have been part of mathlib for quite some time. However, as we were working on adding the basics of functional analysis to mathlib, a drawback quickly became apparent: conjugate-linear maps could not directly be expressed as linear maps. This meant that some constructions could not be formulated in their most natural way: for example, the map that takes an operator to its adjoint on a complex Hilbert space is a conjugate linear map, and so is the Riesz representation that maps a vector to its dual. This was also preventing us from developing the orthogonal group, the unitary group, etc, properly.</p> +Lean community blog (Posts by Frédéric Dupuis)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssSemilinear mapshttps://leanprover-community.github.io/blog/posts/semilinear-maps/Frédéric Dupuis<div><p>Since linear maps appear everywhere in mathematics, it comes as no surprise that they have been part of mathlib for quite some time. However, as we were working on adding the basics of functional analysis to mathlib, a drawback quickly became apparent: conjugate-linear maps could not directly be expressed as linear maps. This meant that some constructions could not be formulated in their most natural way: for example, the map that takes an operator to its adjoint on a complex Hilbert space is a conjugate linear map, and so is the Riesz representation that maps a vector to its dual. This was also preventing us from developing the orthogonal group, the unitary group, etc, properly.</p> <p><a href="https://leanprover-community.github.io/blog/posts/semilinear-maps/">Read more…</a> (4 min remaining to read)</p></div>https://leanprover-community.github.io/blog/posts/semilinear-maps/Sat, 11 Dec 2021 11:00:00 GMT \ No newline at end of file diff --git a/docs/authors/heather-macbeth.xml b/docs/authors/heather-macbeth.xml index f3337bd6..39f66232 100644 --- a/docs/authors/heather-macbeth.xml +++ b/docs/authors/heather-macbeth.xml @@ -1,5 +1,5 @@ -Lean community blog (Posts by Heather Macbeth)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:22 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssClassification of one-dimensional isocrystalshttps://leanprover-community.github.io/blog/posts/classification-of-one-dimensional-isocrystals/Robert Y. Lewis, Heather Macbeth<div><p>Last year, there was a <a href="https://leanprover-community.github.io/blog/posts/semilinear-maps">big mathlib refactor</a> to replace linear maps throughout the library with <em>semilinear maps</em>, +Lean community blog (Posts by Heather Macbeth)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssClassification of one-dimensional isocrystalshttps://leanprover-community.github.io/blog/posts/classification-of-one-dimensional-isocrystals/Robert Y. Lewis, Heather Macbeth<div><p>Last year, there was a <a href="https://leanprover-community.github.io/blog/posts/semilinear-maps">big mathlib refactor</a> to replace linear maps throughout the library with <em>semilinear maps</em>, a more abstract concept which, importantly, unifies linear and conjugate-linear maps.</p> <p>But this is not the full extent of the generalization! Our number theorist friends here in mathlib told us that we should make sure we chose this full generality of <em>semilinear</em> maps, maps $f:M \to N$ such that $f(ax)=\sigma(a)f(x)$ for some ring homomorphism $\sigma$ between the scalar rings of the modules $M$ and $N$. So we and our coauthor Frédéric Dupuis implemented this full generality, and then asked them for an example to illustrate their need for this more abstract definition. This blog post tells the story of our little adventure in number theory.</p> diff --git a/docs/authors/index.html b/docs/authors/index.html index 0669416f..6b5714e5 100644 --- a/docs/authors/index.html +++ b/docs/authors/index.html @@ -49,6 +49,7 @@
    • Anne Baanen
    • Chris Birkbeck
    • David Chanin
      • +
    • Emily Riehl
    • Frédéric Dupuis
    • Heather Macbeth
    • Jana Göken
      • diff --git a/docs/authors/jana-goken.xml b/docs/authors/jana-goken.xml index 0409c5d2..41e169d8 100644 --- a/docs/authors/jana-goken.xml +++ b/docs/authors/jana-goken.xml @@ -1,4 +1,4 @@ -Lean community blog (Posts by Jana Göken)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:22 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssMy Experience at the Machine-Checked Mathematics workshophttps://leanprover-community.github.io/blog/posts/lorentz-center-meeting/Jana Göken<div><p>Hello, everyone! My name is Jana Göken, a master's student in mathematics from Bremen. Today, I want to share with you my experiences at the <a href="https://www.lorentzcenter.nl/machine-checked-mathematics.html">Machine-Checked Mathematics workshop</a> that introduced me to the world of proof assistants, specifically Lean. +Lean community blog (Posts by Jana Göken)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssMy Experience at the Machine-Checked Mathematics workshophttps://leanprover-community.github.io/blog/posts/lorentz-center-meeting/Jana Göken<div><p>Hello, everyone! My name is Jana Göken, a master's student in mathematics from Bremen. Today, I want to share with you my experiences at the <a href="https://www.lorentzcenter.nl/machine-checked-mathematics.html">Machine-Checked Mathematics workshop</a> that introduced me to the world of proof assistants, specifically Lean. The workshop took place in Leiden from July 10th to July 14th 2023, and it was an amazing and educational journey.</p> <p><a href="https://leanprover-community.github.io/blog/posts/lorentz-center-meeting/">Read more…</a> (4 min remaining to read)</p></div>https://leanprover-community.github.io/blog/posts/lorentz-center-meeting/Sat, 26 Aug 2023 14:30:00 GMT \ No newline at end of file diff --git a/docs/authors/jeremy-avigad.xml b/docs/authors/jeremy-avigad.xml index 2573957a..0049cc27 100644 --- a/docs/authors/jeremy-avigad.xml +++ b/docs/authors/jeremy-avigad.xml @@ -1,5 +1,5 @@ -Lean community blog (Posts by Jeremy Avigad)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:21 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssHoskinson Center announcedhttps://leanprover-community.github.io/blog/posts/hoskinson-center-announced/Jeremy Avigad<div><p>On September 22, 2021, Carnegie Mellon University announced that a $20 million gift +Lean community blog (Posts by Jeremy Avigad)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssHoskinson Center announcedhttps://leanprover-community.github.io/blog/posts/hoskinson-center-announced/Jeremy Avigad<div><p>On September 22, 2021, Carnegie Mellon University announced that a $20 million gift from blockchain entrepreneur Charles C. Hoskinson will be used to establish the Hoskinson Center for Formal Mathematics, housed in the Department of Philosophy. You can read the <a href="https://www.cmu.edu/news/stories/archives/2021/september/hoskinson-center-for-formal-mathematics.html">university press release</a> and diff --git a/docs/authors/johan-commelin.xml b/docs/authors/johan-commelin.xml index 61180c97..e91dd8a1 100644 --- a/docs/authors/johan-commelin.xml +++ b/docs/authors/johan-commelin.xml @@ -1,5 +1,5 @@ -Lean community blog (Posts by Johan Commelin)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:21 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssBackstage with Yakov Pecherskyhttps://leanprover-community.github.io/blog/posts/backstage-with-pechersky/Johan Commelin<div><p><a href="https://leanprover-community.github.io/blog/images/yakov_pechersky.png" class="image-reference"><img src="https://leanprover-community.github.io/blog/images/yakov_pechersky.thumbnail.png" class=" align-right"></a></p> +Lean community blog (Posts by Johan Commelin)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssBackstage with Yakov Pecherskyhttps://leanprover-community.github.io/blog/posts/backstage-with-pechersky/Johan Commelin<div><p><a href="https://leanprover-community.github.io/blog/images/yakov_pechersky.png" class="image-reference"><img src="https://leanprover-community.github.io/blog/images/yakov_pechersky.thumbnail.png" class=" align-right"></a></p> <p>The next installment in the series of backstage interviews with mathlib's active contributors!</p> <p>Today, Johan Commelin interviews Yakov Pechersky. diff --git a/docs/authors/kevin-buzzard.xml b/docs/authors/kevin-buzzard.xml index c235f2a4..2c28ca4a 100644 --- a/docs/authors/kevin-buzzard.xml +++ b/docs/authors/kevin-buzzard.xml @@ -1,4 +1,4 @@ -Lean community blog (Posts by Kevin Buzzard)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:22 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssThe Fermat's Last Theorem Projecthttps://leanprover-community.github.io/blog/posts/FLT-announcement/Kevin Buzzard<div><p>Kevin Buzzard discusses the project to prove Fermat's Last Theorem in Lean.</p> +Lean community blog (Posts by Kevin Buzzard)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssThe Fermat's Last Theorem Projecthttps://leanprover-community.github.io/blog/posts/FLT-announcement/Kevin Buzzard<div><p>Kevin Buzzard discusses the project to prove Fermat's Last Theorem in Lean.</p> <p><a href="https://leanprover-community.github.io/blog/posts/FLT-announcement/">Read more…</a> (5 min remaining to read)</p></div>https://leanprover-community.github.io/blog/posts/FLT-announcement/Tue, 30 Apr 2024 18:00:00 GMTFormalising cohomology theorieshttps://leanprover-community.github.io/blog/posts/banff-cohomology/Kevin Buzzard<div><p>Kevin Buzzard rounds up the BIRS conference on formalising cohomology theories.</p> <p><a href="https://leanprover-community.github.io/blog/posts/banff-cohomology/">Read more…</a> (6 min remaining to read)</p></div>https://leanprover-community.github.io/blog/posts/banff-cohomology/Mon, 12 Jun 2023 07:42:45 GMT \ No newline at end of file diff --git a/docs/authors/kexing-ying.xml b/docs/authors/kexing-ying.xml index 71a521ab..76b8f21b 100644 --- a/docs/authors/kexing-ying.xml +++ b/docs/authors/kexing-ying.xml @@ -1,5 +1,5 @@ -Lean community blog (Posts by Kexing Ying)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:21 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssThe Radon-Nikodym theorem in Leanhttps://leanprover-community.github.io/blog/posts/the-radon-nikodym-theorem-in-lean/Kexing Ying<div><p>I have for the past two months been working on formalising the Radon-Nikodym theorem +Lean community blog (Posts by Kexing Ying)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssThe Radon-Nikodym theorem in Leanhttps://leanprover-community.github.io/blog/posts/the-radon-nikodym-theorem-in-lean/Kexing Ying<div><p>I have for the past two months been working on formalising the Radon-Nikodym theorem in Lean, and with <a href="https://github.com/leanprover-community/mathlib/pull/9065">PR #9065</a> merged into mathlib, this journey seems to have finally come to an end. </p> <p><a href="https://leanprover-community.github.io/blog/posts/the-radon-nikodym-theorem-in-lean/">Read more…</a> (5 min remaining to read)</p></div>https://leanprover-community.github.io/blog/posts/the-radon-nikodym-theorem-in-lean/Wed, 22 Sep 2021 10:51:14 GMT \ No newline at end of file diff --git a/docs/authors/mathlib-community.xml b/docs/authors/mathlib-community.xml index de8319c1..58e4f32a 100644 --- a/docs/authors/mathlib-community.xml +++ b/docs/authors/mathlib-community.xml @@ -1,5 +1,5 @@ -Lean community blog (Posts by Mathlib community)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:22 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssThis month in Mathlib (May 2024)https://leanprover-community.github.io/blog/posts/month-in-mathlib/2024/month-in-mathlib-may-2024/Mathlib community<div><p>The last Month in Mathlib posts date from before the port started, in November 2022. We apologise for the momentary disappearance. We aim to keep it a monthly occurrence from now on.</p> +Lean community blog (Posts by Mathlib community)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssThis month in Mathlib (May 2024)https://leanprover-community.github.io/blog/posts/month-in-mathlib/2024/month-in-mathlib-may-2024/Mathlib community<div><p>The last Month in Mathlib posts date from before the port started, in November 2022. We apologise for the momentary disappearance. We aim to keep it a monthly occurrence from now on.</p> <p>There were 667 PRs merged in May 2024.</p> <p><a href="https://leanprover-community.github.io/blog/posts/month-in-mathlib/2024/month-in-mathlib-may-2024/">Read more…</a> (11 min remaining to read)</p></div>https://leanprover-community.github.io/blog/posts/month-in-mathlib/2024/month-in-mathlib-may-2024/Mon, 01 Jul 2024 12:00:00 GMTThis month in mathlib (Sep 2022)https://leanprover-community.github.io/blog/posts/month-in-mathlib/2022/month-in-mathlib-sep-2022/Mathlib community<div><p>In September 2022 there were 361 PRs merged into mathlib. We list some of the highlights below.</p> <p><a href="https://leanprover-community.github.io/blog/posts/month-in-mathlib/2022/month-in-mathlib-sep-2022/">Read more…</a> (1 min remaining to read)</p></div>https://leanprover-community.github.io/blog/posts/month-in-mathlib/2022/month-in-mathlib-sep-2022/Sat, 08 Oct 2022 06:01:27 GMTThis month in mathlib (Aug 2022)https://leanprover-community.github.io/blog/posts/month-in-mathlib/2022/month-in-mathlib-aug-2022/Mathlib community<div><p>In August 2022 there were 506 PRs merged into mathlib. We list some of the highlights below.</p> diff --git a/docs/authors/patrick-massot.xml b/docs/authors/patrick-massot.xml index 6cbec256..f0180cdf 100644 --- a/docs/authors/patrick-massot.xml +++ b/docs/authors/patrick-massot.xml @@ -1,5 +1,5 @@ -Lean community blog (Posts by Patrick Massot)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:22 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssAlex Best’s type class generalization paperhttps://leanprover-community.github.io/blog/posts/alex-bests-type-class-generalization-paper/Patrick Massot<div><p>Alex J. Best wrote a +Lean community blog (Posts by Patrick Massot)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssAlex Best’s type class generalization paperhttps://leanprover-community.github.io/blog/posts/alex-bests-type-class-generalization-paper/Patrick Massot<div><p>Alex J. Best wrote a <a href="https://easychair.org/publications/preprint/KLfT">paper about type class generalization</a> for the <a href="https://cicm-conference.org/2021/">CICM 2021</a> conference on intelligent computer mathematics. </p> diff --git a/docs/authors/riccardo-brasca.xml b/docs/authors/riccardo-brasca.xml index 8676de21..da65b266 100644 --- a/docs/authors/riccardo-brasca.xml +++ b/docs/authors/riccardo-brasca.xml @@ -1,5 +1,5 @@ -Lean community blog (Posts by Riccardo Brasca)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:21 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssThe ring of integers of a cyclotomic fieldhttps://leanprover-community.github.io/blog/posts/the-ring-of-integers-of-a-cyclotomic-field/Riccardo Brasca<div><p>In <a href="https://github.com/leanprover-community/mathlib/pull/13585">PR #13585</a> we compute the +Lean community blog (Posts by Riccardo Brasca)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssThe ring of integers of a cyclotomic fieldhttps://leanprover-community.github.io/blog/posts/the-ring-of-integers-of-a-cyclotomic-field/Riccardo Brasca<div><p>In <a href="https://github.com/leanprover-community/mathlib/pull/13585">PR #13585</a> we compute the discriminant of cyclotomic fields. This is an important result, usually treated in a first year graduate course in number theory. In this post we would like to explain why it is an important result, and briefly explain how we proved it.</p> diff --git a/docs/authors/robert-y-lewis.xml b/docs/authors/robert-y-lewis.xml index 181f0452..5aab860f 100644 --- a/docs/authors/robert-y-lewis.xml +++ b/docs/authors/robert-y-lewis.xml @@ -1,5 +1,5 @@ -Lean community blog (Posts by Robert Y. Lewis)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:21 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssClassification of one-dimensional isocrystalshttps://leanprover-community.github.io/blog/posts/classification-of-one-dimensional-isocrystals/Robert Y. Lewis, Heather Macbeth<div><p>Last year, there was a <a href="https://leanprover-community.github.io/blog/posts/semilinear-maps">big mathlib refactor</a> to replace linear maps throughout the library with <em>semilinear maps</em>, +Lean community blog (Posts by Robert Y. Lewis)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssClassification of one-dimensional isocrystalshttps://leanprover-community.github.io/blog/posts/classification-of-one-dimensional-isocrystals/Robert Y. Lewis, Heather Macbeth<div><p>Last year, there was a <a href="https://leanprover-community.github.io/blog/posts/semilinear-maps">big mathlib refactor</a> to replace linear maps throughout the library with <em>semilinear maps</em>, a more abstract concept which, importantly, unifies linear and conjugate-linear maps.</p> <p>But this is not the full extent of the generalization! Our number theorist friends here in mathlib told us that we should make sure we chose this full generality of <em>semilinear</em> maps, maps $f:M \to N$ such that $f(ax)=\sigma(a)f(x)$ for some ring homomorphism $\sigma$ between the scalar rings of the modules $M$ and $N$. So we and our coauthor Frédéric Dupuis implemented this full generality, and then asked them for an example to illustrate their need for this more abstract definition. This blog post tells the story of our little adventure in number theory.</p> diff --git a/docs/authors/scott-morrison.xml b/docs/authors/scott-morrison.xml index 390383fb..e2bf557c 100644 --- a/docs/authors/scott-morrison.xml +++ b/docs/authors/scott-morrison.xml @@ -1,5 +1,5 @@ -Lean community blog (Posts by Scott Morrison)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:22 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssThe first official release of Lean 4https://leanprover-community.github.io/blog/posts/first-lean-release/Scott Morrison<div><p>Lean 4 has just made its first official stable release, with the arrival of <a href="https://github.com/leanprover/lean4/releases/tag/v4.0.0"><code>v4.0.0</code></a>. +Lean community blog (Posts by Scott Morrison)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssThe first official release of Lean 4https://leanprover-community.github.io/blog/posts/first-lean-release/Scott Morrison<div><p>Lean 4 has just made its first official stable release, with the arrival of <a href="https://github.com/leanprover/lean4/releases/tag/v4.0.0"><code>v4.0.0</code></a>. We're excited to transition from only providing nightly releases to having regular stable releases.</p> <p><a href="https://leanprover-community.github.io/blog/posts/first-lean-release/">Read more…</a> (1 min remaining to read)</p></div>https://leanprover-community.github.io/blog/posts/first-lean-release/Fri, 08 Sep 2023 05:58:40 GMTUpdate on mathport (Dec 2021)https://leanprover-community.github.io/blog/posts/intro-to-mathport/Scott Morrison<div><p><code>mathport</code> is the tool we're planning on using to help us port <code>mathlib</code> to Lean 4. It has mostly been written by Mario Carneiro and Daniel Selsam, diff --git a/docs/authors/the-lean-prover-community.xml b/docs/authors/the-lean-prover-community.xml index 59dcac67..bcade91a 100644 --- a/docs/authors/the-lean-prover-community.xml +++ b/docs/authors/the-lean-prover-community.xml @@ -1,5 +1,5 @@ -Lean community blog (Posts by The Lean prover community)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:21 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssThis month in mathlib (Oct and Nov 2022)https://leanprover-community.github.io/blog/posts/month-in-mathlib/2022/month-in-mathlib-oct-and-nov-2022/The Lean prover community<div><p>In October and November 2022 there were 512 and 453 PRs merged into mathlib. We list some of the highlights below.</p> +Lean community blog (Posts by The Lean prover community)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssThis month in mathlib (Oct and Nov 2022)https://leanprover-community.github.io/blog/posts/month-in-mathlib/2022/month-in-mathlib-oct-and-nov-2022/The Lean prover community<div><p>In October and November 2022 there were 512 and 453 PRs merged into mathlib. We list some of the highlights below.</p> <ul> <li> <p>Measure theory.</p> diff --git a/docs/authors/yury-kudryashov.xml b/docs/authors/yury-kudryashov.xml index 31a3f94e..1a39952a 100644 --- a/docs/authors/yury-kudryashov.xml +++ b/docs/authors/yury-kudryashov.xml @@ -1,5 +1,5 @@ -Lean community blog (Posts by Yury Kudryashov)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:21 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssAdventure 10000https://leanprover-community.github.io/blog/posts/adventure-10000/Yury Kudryashov<div><p>About a month ago, the <a href="https://en.wikipedia.org/wiki/Cauchy%27s_integral_theorem">Cauchy integral +Lean community blog (Posts by Yury Kudryashov)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssAdventure 10000https://leanprover-community.github.io/blog/posts/adventure-10000/Yury Kudryashov<div><p>About a month ago, the <a href="https://en.wikipedia.org/wiki/Cauchy%27s_integral_theorem">Cauchy integral theorem</a> for some simple domains <a href="https://github.com/leanprover-community/mathlib/pull/10000">landed</a> diff --git a/docs/categories/-cosmos.xml b/docs/categories/-cosmos.xml new file mode 100644 index 00000000..9125d54c --- /dev/null +++ b/docs/categories/-cosmos.xml @@ -0,0 +1,3 @@ + +Lean community blog (Posts about ∞-Cosmos)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssAnnouncing the ∞-Cosmos Projecthttps://leanprover-community.github.io/blog/posts/infinity-cosmos-announcement/Emily Riehl<div><p><a href="https://github.com/emilyriehl">Emily Riehl</a> introduces the <a href="https://github.com/emilyriehl/infinity-cosmos">∞-Cosmos Project</a>.</p> +<p><a href="https://leanprover-community.github.io/blog/posts/infinity-cosmos-announcement/">Read more…</a> (2 min remaining to read)</p></div>∞-Cosmoshttps://leanprover-community.github.io/blog/posts/infinity-cosmos-announcement/Tue, 17 Sep 2024 18:00:00 GMT \ No newline at end of file diff --git a/docs/categories/-cosmos/index.html b/docs/categories/-cosmos/index.html new file mode 100644 index 00000000..21a990c8 --- /dev/null +++ b/docs/categories/-cosmos/index.html @@ -0,0 +1,66 @@ + + + + + +Posts about ∞-Cosmos | Lean community blog + + + + + + + + + + + + + + + + + Skip to main content +
      +

      Contents © 2024 The Lean prover community - Powered by Nikola

      + +
      +
      + + + + + + diff --git a/docs/categories/backstage.xml b/docs/categories/backstage.xml index 8dfbb0cd..a2d58f3b 100644 --- a/docs/categories/backstage.xml +++ b/docs/categories/backstage.xml @@ -1,5 +1,5 @@ -Lean community blog (Posts about backstage)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:21 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssBackstage with Yakov Pecherskyhttps://leanprover-community.github.io/blog/posts/backstage-with-pechersky/Johan Commelin<div><p><a href="https://leanprover-community.github.io/blog/images/yakov_pechersky.png" class="image-reference"><img src="https://leanprover-community.github.io/blog/images/yakov_pechersky.thumbnail.png" class=" align-right"></a></p> +Lean community blog (Posts about backstage)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssBackstage with Yakov Pecherskyhttps://leanprover-community.github.io/blog/posts/backstage-with-pechersky/Johan Commelin<div><p><a href="https://leanprover-community.github.io/blog/images/yakov_pechersky.png" class="image-reference"><img src="https://leanprover-community.github.io/blog/images/yakov_pechersky.thumbnail.png" class=" align-right"></a></p> <p>The next installment in the series of backstage interviews with mathlib's active contributors!</p> <p>Today, Johan Commelin interviews Yakov Pechersky. diff --git a/docs/categories/cat_announcement.xml b/docs/categories/cat_announcement.xml index 0a529ddc..9c1fc046 100644 --- a/docs/categories/cat_announcement.xml +++ b/docs/categories/cat_announcement.xml @@ -1,4 +1,4 @@ -Lean community blog (Posts about announcement)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:22 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssThe first official release of Lean 4https://leanprover-community.github.io/blog/posts/first-lean-release/Scott Morrison<div><p>Lean 4 has just made its first official stable release, with the arrival of <a href="https://github.com/leanprover/lean4/releases/tag/v4.0.0"><code>v4.0.0</code></a>. +Lean community blog (Posts about announcement)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssThe first official release of Lean 4https://leanprover-community.github.io/blog/posts/first-lean-release/Scott Morrison<div><p>Lean 4 has just made its first official stable release, with the arrival of <a href="https://github.com/leanprover/lean4/releases/tag/v4.0.0"><code>v4.0.0</code></a>. We're excited to transition from only providing nightly releases to having regular stable releases.</p> <p><a href="https://leanprover-community.github.io/blog/posts/first-lean-release/">Read more…</a> (1 min remaining to read)</p></div>https://leanprover-community.github.io/blog/posts/first-lean-release/Fri, 08 Sep 2023 05:58:40 GMT \ No newline at end of file diff --git a/docs/categories/cat_announcements.xml b/docs/categories/cat_announcements.xml index 110f8032..f5065ce0 100644 --- a/docs/categories/cat_announcements.xml +++ b/docs/categories/cat_announcements.xml @@ -1,5 +1,5 @@ -Lean community blog (Posts about Announcements)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:21 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssHoskinson Center announcedhttps://leanprover-community.github.io/blog/posts/hoskinson-center-announced/Jeremy Avigad<div><p>On September 22, 2021, Carnegie Mellon University announced that a $20 million gift +Lean community blog (Posts about Announcements)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssHoskinson Center announcedhttps://leanprover-community.github.io/blog/posts/hoskinson-center-announced/Jeremy Avigad<div><p>On September 22, 2021, Carnegie Mellon University announced that a $20 million gift from blockchain entrepreneur Charles C. Hoskinson will be used to establish the Hoskinson Center for Formal Mathematics, housed in the Department of Philosophy. You can read the <a href="https://www.cmu.edu/news/stories/archives/2021/september/hoskinson-center-for-formal-mathematics.html">university press release</a> and diff --git a/docs/categories/cat_community-projects.xml b/docs/categories/cat_community-projects.xml index 003590d6..a1a9b40b 100644 --- a/docs/categories/cat_community-projects.xml +++ b/docs/categories/cat_community-projects.xml @@ -1,5 +1,5 @@ -Lean community blog (Posts about Community projects)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:21 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssDefinitions in the liquid tensor experimenthttps://leanprover-community.github.io/blog/posts/lte-examples/Adam Topaz<div><p>A few weeks ago, we announced the <a href="https://leanprover-community.github.io/blog/posts/lte-final/">completion of the liquid tensor experiment</a> (<strong>LTE</strong> for short). +Lean community blog (Posts about Community projects)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssDefinitions in the liquid tensor experimenthttps://leanprover-community.github.io/blog/posts/lte-examples/Adam Topaz<div><p>A few weeks ago, we announced the <a href="https://leanprover-community.github.io/blog/posts/lte-final/">completion of the liquid tensor experiment</a> (<strong>LTE</strong> for short). What this means is that we stated and (completely) proved the following result in Lean:</p> <pre class="code literal-block"><span class="kd">variables</span> <span class="o">(</span><span class="n">p'</span> <span class="n">p</span> <span class="o">:</span> <span class="n">ℝ</span><span class="bp">≥</span><span class="mi">0</span><span class="o">)</span> <span class="o">[</span><span class="n">fact</span> <span class="o">(</span><span class="mi">0</span> <span class="bp">&lt;</span> <span class="n">p'</span><span class="o">)]</span> <span class="o">[</span><span class="n">fact</span> <span class="o">(</span><span class="n">p'</span> <span class="bp">&lt;</span> <span class="n">p</span><span class="o">)]</span> <span class="o">[</span><span class="n">fact</span> <span class="o">(</span><span class="n">p</span> <span class="bp">≤</span> <span class="mi">1</span><span class="o">)]</span> diff --git a/docs/categories/cat_interviews.xml b/docs/categories/cat_interviews.xml index 5452735d..8f996ade 100644 --- a/docs/categories/cat_interviews.xml +++ b/docs/categories/cat_interviews.xml @@ -1,5 +1,5 @@ -Lean community blog (Posts about Interviews)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:22 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssBackstage with Yakov Pecherskyhttps://leanprover-community.github.io/blog/posts/backstage-with-pechersky/Johan Commelin<div><p><a href="https://leanprover-community.github.io/blog/images/yakov_pechersky.png" class="image-reference"><img src="https://leanprover-community.github.io/blog/images/yakov_pechersky.thumbnail.png" class=" align-right"></a></p> +Lean community blog (Posts about Interviews)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssBackstage with Yakov Pecherskyhttps://leanprover-community.github.io/blog/posts/backstage-with-pechersky/Johan Commelin<div><p><a href="https://leanprover-community.github.io/blog/images/yakov_pechersky.png" class="image-reference"><img src="https://leanprover-community.github.io/blog/images/yakov_pechersky.thumbnail.png" class=" align-right"></a></p> <p>The next installment in the series of backstage interviews with mathlib's active contributors!</p> <p>Today, Johan Commelin interviews Yakov Pechersky. diff --git a/docs/categories/cat_mathport.xml b/docs/categories/cat_mathport.xml index 93f8d79a..598a1368 100644 --- a/docs/categories/cat_mathport.xml +++ b/docs/categories/cat_mathport.xml @@ -1,5 +1,5 @@ -Lean community blog (Posts about mathport)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:22 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssUpdate on mathport (Dec 2021)https://leanprover-community.github.io/blog/posts/intro-to-mathport/Scott Morrison<div><p><code>mathport</code> is the tool we're planning on using to help us port <code>mathlib</code> to Lean 4. +Lean community blog (Posts about mathport)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssUpdate on mathport (Dec 2021)https://leanprover-community.github.io/blog/posts/intro-to-mathport/Scott Morrison<div><p><code>mathport</code> is the tool we're planning on using to help us port <code>mathlib</code> to Lean 4. It has mostly been written by Mario Carneiro and Daniel Selsam, and Gabriel Ebner and I have been making some fixes.</p> <p>To provide some context, <a href="https://github.com/leanprover-community/mathlib">mathlib</a> diff --git a/docs/categories/cat_meeting-report.xml b/docs/categories/cat_meeting-report.xml index 631bb1a7..cf1fcb3b 100644 --- a/docs/categories/cat_meeting-report.xml +++ b/docs/categories/cat_meeting-report.xml @@ -1,5 +1,5 @@ -Lean community blog (Posts about meeting report)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:22 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssMy Experience at the Machine-Checked Mathematics workshophttps://leanprover-community.github.io/blog/posts/lorentz-center-meeting/Jana Göken<div><p>Hello, everyone! My name is Jana Göken, a master's student in mathematics from Bremen. Today, I want to share with you my experiences at the <a href="https://www.lorentzcenter.nl/machine-checked-mathematics.html">Machine-Checked Mathematics workshop</a> that introduced me to the world of proof assistants, specifically Lean. +Lean community blog (Posts about meeting report)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssMy Experience at the Machine-Checked Mathematics workshophttps://leanprover-community.github.io/blog/posts/lorentz-center-meeting/Jana Göken<div><p>Hello, everyone! My name is Jana Göken, a master's student in mathematics from Bremen. Today, I want to share with you my experiences at the <a href="https://www.lorentzcenter.nl/machine-checked-mathematics.html">Machine-Checked Mathematics workshop</a> that introduced me to the world of proof assistants, specifically Lean. The workshop took place in Leiden from July 10th to July 14th 2023, and it was an amazing and educational journey.</p> <p><a href="https://leanprover-community.github.io/blog/posts/lorentz-center-meeting/">Read more…</a> (4 min remaining to read)</p></div>https://leanprover-community.github.io/blog/posts/lorentz-center-meeting/Sat, 26 Aug 2023 14:30:00 GMTFormalising cohomology theorieshttps://leanprover-community.github.io/blog/posts/banff-cohomology/Kevin Buzzard<div><p>Kevin Buzzard rounds up the BIRS conference on formalising cohomology theories.</p> <p><a href="https://leanprover-community.github.io/blog/posts/banff-cohomology/">Read more…</a> (6 min remaining to read)</p></div>https://leanprover-community.github.io/blog/posts/banff-cohomology/Mon, 12 Jun 2023 07:42:45 GMT \ No newline at end of file diff --git a/docs/categories/cat_month-in-mathlib.xml b/docs/categories/cat_month-in-mathlib.xml index d0b9018a..81c27f30 100644 --- a/docs/categories/cat_month-in-mathlib.xml +++ b/docs/categories/cat_month-in-mathlib.xml @@ -1,5 +1,5 @@ -Lean community blog (Posts about month-in-mathlib)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:22 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssThis month in Mathlib (May 2024)https://leanprover-community.github.io/blog/posts/month-in-mathlib/2024/month-in-mathlib-may-2024/Mathlib community<div><p>The last Month in Mathlib posts date from before the port started, in November 2022. We apologise for the momentary disappearance. We aim to keep it a monthly occurrence from now on.</p> +Lean community blog (Posts about month-in-mathlib)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssThis month in Mathlib (May 2024)https://leanprover-community.github.io/blog/posts/month-in-mathlib/2024/month-in-mathlib-may-2024/Mathlib community<div><p>The last Month in Mathlib posts date from before the port started, in November 2022. We apologise for the momentary disappearance. We aim to keep it a monthly occurrence from now on.</p> <p>There were 667 PRs merged in May 2024.</p> <p><a href="https://leanprover-community.github.io/blog/posts/month-in-mathlib/2024/month-in-mathlib-may-2024/">Read more…</a> (11 min remaining to read)</p></div>https://leanprover-community.github.io/blog/posts/month-in-mathlib/2024/month-in-mathlib-may-2024/Mon, 01 Jul 2024 12:00:00 GMTThis month in mathlib (Oct and Nov 2022)https://leanprover-community.github.io/blog/posts/month-in-mathlib/2022/month-in-mathlib-oct-and-nov-2022/The Lean prover community<div><p>In October and November 2022 there were 512 and 453 PRs merged into mathlib. We list some of the highlights below.</p> <ul> diff --git a/docs/categories/cat_new-in-mathlib.xml b/docs/categories/cat_new-in-mathlib.xml index ad5054d1..975a977d 100644 --- a/docs/categories/cat_new-in-mathlib.xml +++ b/docs/categories/cat_new-in-mathlib.xml @@ -1,5 +1,5 @@ -Lean community blog (Posts about New in mathlib)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:21 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssModular formshttps://leanprover-community.github.io/blog/posts/modular-forms/Chris Birkbeck<div><p>In <a href="https://github.com/leanprover-community/mathlib/pull/13250">PR# 13250</a> we define modular forms and cusp forms, and prove that they form complex vector spaces. These are analytic functions of number theoretic interest with strong links to geometry, representation theory and analysis. Most famously they are a key ingredient in the proof of Fermat's Last Theorem. In this post we discuss the formalization process, motivate some design choices and map out some future work.</p> +Lean community blog (Posts about New in mathlib)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssModular formshttps://leanprover-community.github.io/blog/posts/modular-forms/Chris Birkbeck<div><p>In <a href="https://github.com/leanprover-community/mathlib/pull/13250">PR# 13250</a> we define modular forms and cusp forms, and prove that they form complex vector spaces. These are analytic functions of number theoretic interest with strong links to geometry, representation theory and analysis. Most famously they are a key ingredient in the proof of Fermat's Last Theorem. In this post we discuss the formalization process, motivate some design choices and map out some future work.</p> <p><a href="https://leanprover-community.github.io/blog/posts/modular-forms/">Read more…</a> (7 min remaining to read)</p></div>https://leanprover-community.github.io/blog/posts/modular-forms/Wed, 21 Dec 2022 11:41:21 GMTClassification of one-dimensional isocrystalshttps://leanprover-community.github.io/blog/posts/classification-of-one-dimensional-isocrystals/Robert Y. Lewis, Heather Macbeth<div><p>Last year, there was a <a href="https://leanprover-community.github.io/blog/posts/semilinear-maps">big mathlib refactor</a> to replace linear maps throughout the library with <em>semilinear maps</em>, a more abstract concept which, importantly, unifies linear and conjugate-linear maps.</p> <p>But this is not the full extent of the generalization! Our number theorist friends here in mathlib told us that we should diff --git a/docs/categories/cat_overview.xml b/docs/categories/cat_overview.xml index 2c853aca..2b0dc998 100644 --- a/docs/categories/cat_overview.xml +++ b/docs/categories/cat_overview.xml @@ -1,5 +1,5 @@ -Lean community blog (Posts about overview)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:22 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rss2021 - The Bottom Linehttps://leanprover-community.github.io/blog/posts/2021-the-bottom-line/Mathlib community<div><p>Since the mathlib repository was created in summer 2017, +Lean community blog (Posts about overview)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rss2021 - The Bottom Linehttps://leanprover-community.github.io/blog/posts/2021-the-bottom-line/Mathlib community<div><p>Since the mathlib repository was created in summer 2017, each year has been bigger than the last. As an end-of-year retrospective, we look at how the mathlib library and community have developed in 2021.</p> <p><a href="https://leanprover-community.github.io/blog/posts/2021-the-bottom-line/">Read more…</a> (5 min remaining to read)</p></div>https://leanprover-community.github.io/blog/posts/2021-the-bottom-line/Sat, 08 Jan 2022 19:35:59 GMT \ No newline at end of file diff --git a/docs/categories/cat_papers.xml b/docs/categories/cat_papers.xml index 1317c274..550d8f50 100644 --- a/docs/categories/cat_papers.xml +++ b/docs/categories/cat_papers.xml @@ -1,5 +1,5 @@ -Lean community blog (Posts about Papers)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:21 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssAlex Best’s type class generalization paperhttps://leanprover-community.github.io/blog/posts/alex-bests-type-class-generalization-paper/Patrick Massot<div><p>Alex J. Best wrote a +Lean community blog (Posts about Papers)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssAlex Best’s type class generalization paperhttps://leanprover-community.github.io/blog/posts/alex-bests-type-class-generalization-paper/Patrick Massot<div><p>Alex J. Best wrote a <a href="https://easychair.org/publications/preprint/KLfT">paper about type class generalization</a> for the <a href="https://cicm-conference.org/2021/">CICM 2021</a> conference on intelligent computer mathematics. </p> diff --git a/docs/categories/cat_project-announcement.xml b/docs/categories/cat_project-announcement.xml index ec6ede2a..91e05b50 100644 --- a/docs/categories/cat_project-announcement.xml +++ b/docs/categories/cat_project-announcement.xml @@ -1,3 +1,4 @@ -Lean community blog (Posts about project announcement)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Fri, 02 Aug 2024 16:48:22 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssThe Fermat's Last Theorem Projecthttps://leanprover-community.github.io/blog/posts/FLT-announcement/Kevin Buzzard<div><p>Kevin Buzzard discusses the project to prove Fermat's Last Theorem in Lean.</p> +Lean community blog (Posts about project announcement)https://leanprover-community.github.io/blog/enContents © 2024 <a href="mailto:">The Lean prover community</a> Wed, 18 Sep 2024 00:13:43 GMTNikola (getnikola.com)http://blogs.law.harvard.edu/tech/rssAnnouncing the ∞-Cosmos Projecthttps://leanprover-community.github.io/blog/posts/infinity-cosmos-announcement/Emily Riehl<div><p><a href="https://github.com/emilyriehl">Emily Riehl</a> introduces the <a href="https://github.com/emilyriehl/infinity-cosmos">∞-Cosmos Project</a>.</p> +<p><a href="https://leanprover-community.github.io/blog/posts/infinity-cosmos-announcement/">Read more…</a> (2 min remaining to read)</p></div>∞-Cosmoshttps://leanprover-community.github.io/blog/posts/infinity-cosmos-announcement/Tue, 17 Sep 2024 18:00:00 GMTThe Fermat's Last Theorem Projecthttps://leanprover-community.github.io/blog/posts/FLT-announcement/Kevin Buzzard<div><p>Kevin Buzzard discusses the project to prove Fermat's Last Theorem in Lean.</p> <p><a href="https://leanprover-community.github.io/blog/posts/FLT-announcement/">Read more…</a> (5 min remaining to read)</p></div>https://leanprover-community.github.io/blog/posts/FLT-announcement/Tue, 30 Apr 2024 18:00:00 GMT \ No newline at end of file diff --git a/docs/categories/cat_project-announcement/index.html b/docs/categories/cat_project-announcement/index.html index 881428ca..2d27ef1e 100644 --- a/docs/categories/cat_project-announcement/index.html +++ b/docs/categories/cat_project-announcement/index.html @@ -51,6 +51,9 @@