deploy site from 7b20f02

Author: leanprover-community-bot

docs/2024/index.html

@@ -43,6 +43,9 @@
     </ul></nav></header><main id="content"><article class="listpage"><header><h1>Posts for year 2024</h1>
     </header><ul class="postlist">
 <li>
+<time class="listdate" datetime="2024-11-25T17:00:00Z" title="2024-11-25 17:00">2024-11-25 17:00</time><a href="../posts/durham-algebraic-geometry-workshop/" class="listtitle">Durham Computational Algebraic Geometry Workshop</a>
+</li>
+        <li>
 <time class="listdate" datetime="2024-10-17T16:41:48+02:00" title="2024-10-17 16:41">2024-10-17 16:41</time><a href="../posts/basic-probability-in-mathlib/" class="listtitle">Basic probability in Mathlib</a>
 </li>
         <li>

docs/archive.html

@@ -44,7 +44,7 @@
     </header><ul class="postlist">
 <li>
 <a href="2024/">2024</a>
-            (4)
+            (5)
         </li>
 <li>
 <a href="2023/">2023</a>

docs/authors/adam-topaz.xml

@@ -1,5 +1,5 @@
 <?xml version="1.0" encoding="utf-8"?>
-<?xml-stylesheet type="text/xsl" href="../assets/xml/rss.xsl" media="all"?><rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Lean community blog (Posts by Adam Topaz)</title><link>https://leanprover-community.github.io/blog/</link><description></description><atom:link href="https://leanprover-community.github.io/blog/authors/adam-topaz.xml" rel="self" type="application/rss+xml"></atom:link><language>en</language><copyright>Contents © 2024 &lt;a href="mailto:"&gt;The Lean prover community&lt;/a&gt; </copyright><lastBuildDate>Fri, 18 Oct 2024 08:28:43 GMT</lastBuildDate><generator>Nikola (getnikola.com)</generator><docs>http://blogs.law.harvard.edu/tech/rss</docs><item><title>Definitions in the liquid tensor experiment</title><link>https://leanprover-community.github.io/blog/posts/lte-examples/</link><dc:creator>Adam Topaz</dc:creator><description>&lt;div&gt;&lt;p&gt;A few weeks ago, we announced the &lt;a href="https://leanprover-community.github.io/blog/posts/lte-final/"&gt;completion of the liquid tensor experiment&lt;/a&gt; (&lt;strong&gt;LTE&lt;/strong&gt; for short).
+<?xml-stylesheet type="text/xsl" href="../assets/xml/rss.xsl" media="all"?><rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Lean community blog (Posts by Adam Topaz)</title><link>https://leanprover-community.github.io/blog/</link><description></description><atom:link href="https://leanprover-community.github.io/blog/authors/adam-topaz.xml" rel="self" type="application/rss+xml"></atom:link><language>en</language><copyright>Contents © 2024 &lt;a href="mailto:"&gt;The Lean prover community&lt;/a&gt; </copyright><lastBuildDate>Mon, 25 Nov 2024 17:49:59 GMT</lastBuildDate><generator>Nikola (getnikola.com)</generator><docs>http://blogs.law.harvard.edu/tech/rss</docs><item><title>Definitions in the liquid tensor experiment</title><link>https://leanprover-community.github.io/blog/posts/lte-examples/</link><dc:creator>Adam Topaz</dc:creator><description>&lt;div&gt;&lt;p&gt;A few weeks ago, we announced the &lt;a href="https://leanprover-community.github.io/blog/posts/lte-final/"&gt;completion of the liquid tensor experiment&lt;/a&gt; (&lt;strong&gt;LTE&lt;/strong&gt; for short).
 What this means is that we stated and (completely) proved the following result in Lean:&lt;/p&gt;
 &lt;pre class="code literal-block"&gt;&lt;span class="kd"&gt;variables&lt;/span&gt; &lt;span class="o"&gt;(&lt;/span&gt;&lt;span class="n"&gt;p'&lt;/span&gt; &lt;span class="n"&gt;p&lt;/span&gt; &lt;span class="o"&gt;:&lt;/span&gt; &lt;span class="n"&gt;ℝ&lt;/span&gt;&lt;span class="bp"&gt;≥&lt;/span&gt;&lt;span class="mi"&gt;0&lt;/span&gt;&lt;span class="o"&gt;)&lt;/span&gt; &lt;span class="o"&gt;[&lt;/span&gt;&lt;span class="n"&gt;fact&lt;/span&gt; &lt;span class="o"&gt;(&lt;/span&gt;&lt;span class="mi"&gt;0&lt;/span&gt; &lt;span class="bp"&gt;&amp;lt;&lt;/span&gt; &lt;span class="n"&gt;p'&lt;/span&gt;&lt;span class="o"&gt;)]&lt;/span&gt; &lt;span class="o"&gt;[&lt;/span&gt;&lt;span class="n"&gt;fact&lt;/span&gt; &lt;span class="o"&gt;(&lt;/span&gt;&lt;span class="n"&gt;p'&lt;/span&gt; &lt;span class="bp"&gt;&amp;lt;&lt;/span&gt; &lt;span class="n"&gt;p&lt;/span&gt;&lt;span class="o"&gt;)]&lt;/span&gt; &lt;span class="o"&gt;[&lt;/span&gt;&lt;span class="n"&gt;fact&lt;/span&gt; &lt;span class="o"&gt;(&lt;/span&gt;&lt;span class="n"&gt;p&lt;/span&gt; &lt;span class="bp"&gt;≤&lt;/span&gt; &lt;span class="mi"&gt;1&lt;/span&gt;&lt;span class="o"&gt;)]&lt;/span&gt;
 

docs/authors/anne-baanen.xml

@@ -1,5 +1,5 @@
 <?xml version="1.0" encoding="utf-8"?>
-<?xml-stylesheet type="text/xsl" href="../assets/xml/rss.xsl" media="all"?><rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Lean community blog (Posts by Anne Baanen)</title><link>https://leanprover-community.github.io/blog/</link><description></description><atom:link href="https://leanprover-community.github.io/blog/authors/anne-baanen.xml" rel="self" type="application/rss+xml"></atom:link><language>en</language><copyright>Contents © 2024 &lt;a href="mailto:"&gt;The Lean prover community&lt;/a&gt; </copyright><lastBuildDate>Fri, 18 Oct 2024 08:28:43 GMT</lastBuildDate><generator>Nikola (getnikola.com)</generator><docs>http://blogs.law.harvard.edu/tech/rss</docs><item><title>Dedekind domains and class number in Lean</title><link>https://leanprover-community.github.io/blog/posts/dedekind-domains-and-class-number-in-lean/</link><dc:creator>Anne Baanen</dc:creator><description>&lt;div&gt;&lt;p&gt;Pull request &lt;a href="https://github.com/leanprover-community/mathlib/pull/9071"&gt;#9701&lt;/a&gt; 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).
+<?xml-stylesheet type="text/xsl" href="../assets/xml/rss.xsl" media="all"?><rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Lean community blog (Posts by Anne Baanen)</title><link>https://leanprover-community.github.io/blog/</link><description></description><atom:link href="https://leanprover-community.github.io/blog/authors/anne-baanen.xml" rel="self" type="application/rss+xml"></atom:link><language>en</language><copyright>Contents © 2024 &lt;a href="mailto:"&gt;The Lean prover community&lt;/a&gt; </copyright><lastBuildDate>Mon, 25 Nov 2024 17:49:59 GMT</lastBuildDate><generator>Nikola (getnikola.com)</generator><docs>http://blogs.law.harvard.edu/tech/rss</docs><item><title>Dedekind domains and class number in Lean</title><link>https://leanprover-community.github.io/blog/posts/dedekind-domains-and-class-number-in-lean/</link><dc:creator>Anne Baanen</dc:creator><description>&lt;div&gt;&lt;p&gt;Pull request &lt;a href="https://github.com/leanprover-community/mathlib/pull/9071"&gt;#9701&lt;/a&gt; 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:

docs/authors/chris-birkbeck.xml

@@ -1,3 +1,3 @@
 <?xml version="1.0" encoding="utf-8"?>
-<?xml-stylesheet type="text/xsl" href="../assets/xml/rss.xsl" media="all"?><rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Lean community blog (Posts by Chris Birkbeck)</title><link>https://leanprover-community.github.io/blog/</link><description></description><atom:link href="https://leanprover-community.github.io/blog/authors/chris-birkbeck.xml" rel="self" type="application/rss+xml"></atom:link><language>en</language><copyright>Contents © 2024 &lt;a href="mailto:"&gt;The Lean prover community&lt;/a&gt; </copyright><lastBuildDate>Fri, 18 Oct 2024 08:28:43 GMT</lastBuildDate><generator>Nikola (getnikola.com)</generator><docs>http://blogs.law.harvard.edu/tech/rss</docs><item><title>Modular forms</title><link>https://leanprover-community.github.io/blog/posts/modular-forms/</link><dc:creator>Chris Birkbeck</dc:creator><description>&lt;div&gt;&lt;p&gt;In &lt;a href="https://github.com/leanprover-community/mathlib/pull/13250"&gt;PR# 13250&lt;/a&gt; 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.&lt;/p&gt;
+<?xml-stylesheet type="text/xsl" href="../assets/xml/rss.xsl" media="all"?><rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Lean community blog (Posts by Chris Birkbeck)</title><link>https://leanprover-community.github.io/blog/</link><description></description><atom:link href="https://leanprover-community.github.io/blog/authors/chris-birkbeck.xml" rel="self" type="application/rss+xml"></atom:link><language>en</language><copyright>Contents © 2024 &lt;a href="mailto:"&gt;The Lean prover community&lt;/a&gt; </copyright><lastBuildDate>Mon, 25 Nov 2024 17:49:59 GMT</lastBuildDate><generator>Nikola (getnikola.com)</generator><docs>http://blogs.law.harvard.edu/tech/rss</docs><item><title>Modular forms</title><link>https://leanprover-community.github.io/blog/posts/modular-forms/</link><dc:creator>Chris Birkbeck</dc:creator><description>&lt;div&gt;&lt;p&gt;In &lt;a href="https://github.com/leanprover-community/mathlib/pull/13250"&gt;PR# 13250&lt;/a&gt; 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.&lt;/p&gt;
 &lt;p&gt;&lt;a href="https://leanprover-community.github.io/blog/posts/modular-forms/"&gt;Read more…&lt;/a&gt; (7 min remaining to read)&lt;/p&gt;&lt;/div&gt;</description><guid>https://leanprover-community.github.io/blog/posts/modular-forms/</guid><pubDate>Wed, 21 Dec 2022 11:41:21 GMT</pubDate></item></channel></rss>

docs/authors/david-chanin.xml

@@ -1,4 +1,4 @@
 <?xml version="1.0" encoding="utf-8"?>
-<?xml-stylesheet type="text/xsl" href="../assets/xml/rss.xsl" media="all"?><rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Lean community blog (Posts by David Chanin)</title><link>https://leanprover-community.github.io/blog/</link><description></description><atom:link href="https://leanprover-community.github.io/blog/authors/david-chanin.xml" rel="self" type="application/rss+xml"></atom:link><language>en</language><copyright>Contents © 2024 &lt;a href="mailto:"&gt;The Lean prover community&lt;/a&gt; </copyright><lastBuildDate>Fri, 18 Oct 2024 08:28:43 GMT</lastBuildDate><generator>Nikola (getnikola.com)</generator><docs>http://blogs.law.harvard.edu/tech/rss</docs><item><title>Introducing Mathlib Changelog</title><link>https://leanprover-community.github.io/blog/posts/mathlib-changelog/</link><dc:creator>David Chanin</dc:creator><description>&lt;div&gt;&lt;p&gt;&lt;img alt="mathlib-changelog sample page" src="https://leanprover-community.github.io/blog/images/changelog_lemma.png"&gt;&lt;/p&gt;
+<?xml-stylesheet type="text/xsl" href="../assets/xml/rss.xsl" media="all"?><rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Lean community blog (Posts by David Chanin)</title><link>https://leanprover-community.github.io/blog/</link><description></description><atom:link href="https://leanprover-community.github.io/blog/authors/david-chanin.xml" rel="self" type="application/rss+xml"></atom:link><language>en</language><copyright>Contents © 2024 &lt;a href="mailto:"&gt;The Lean prover community&lt;/a&gt; </copyright><lastBuildDate>Mon, 25 Nov 2024 17:49:59 GMT</lastBuildDate><generator>Nikola (getnikola.com)</generator><docs>http://blogs.law.harvard.edu/tech/rss</docs><item><title>Introducing Mathlib Changelog</title><link>https://leanprover-community.github.io/blog/posts/mathlib-changelog/</link><dc:creator>David Chanin</dc:creator><description>&lt;div&gt;&lt;p&gt;&lt;img alt="mathlib-changelog sample page" src="https://leanprover-community.github.io/blog/images/changelog_lemma.png"&gt;&lt;/p&gt;
 &lt;p&gt;Tldr; check out &lt;a href="https://mathlib-changelog.org"&gt;mathlib-changelog.org&lt;/a&gt; to explore the historical changes to mathlib, and find out what happened to that lemma you were using.&lt;/p&gt;
 &lt;p&gt;&lt;a href="https://leanprover-community.github.io/blog/posts/mathlib-changelog/"&gt;Read more…&lt;/a&gt; (3 min remaining to read)&lt;/p&gt;&lt;/div&gt;</description><guid>https://leanprover-community.github.io/blog/posts/mathlib-changelog/</guid><pubDate>Thu, 28 Jul 2022 07:35:23 GMT</pubDate></item></channel></rss>

docs/authors/emily-riehl.xml

@@ -1,3 +1,3 @@
 <?xml version="1.0" encoding="utf-8"?>
-<?xml-stylesheet type="text/xsl" href="../assets/xml/rss.xsl" media="all"?><rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Lean community blog (Posts by Emily Riehl)</title><link>https://leanprover-community.github.io/blog/</link><description></description><atom:link href="https://leanprover-community.github.io/blog/authors/emily-riehl.xml" rel="self" type="application/rss+xml"></atom:link><language>en</language><copyright>Contents © 2024 &lt;a href="mailto:"&gt;The Lean prover community&lt;/a&gt; </copyright><lastBuildDate>Fri, 18 Oct 2024 08:28:43 GMT</lastBuildDate><generator>Nikola (getnikola.com)</generator><docs>http://blogs.law.harvard.edu/tech/rss</docs><item><title>Announcing the ∞-Cosmos Project</title><link>https://leanprover-community.github.io/blog/posts/infinity-cosmos-announcement/</link><dc:creator>Emily Riehl</dc:creator><description>&lt;div&gt;&lt;p&gt;&lt;a href="https://github.com/emilyriehl"&gt;Emily Riehl&lt;/a&gt; introduces the &lt;a href="https://github.com/emilyriehl/infinity-cosmos"&gt;∞-Cosmos Project&lt;/a&gt;.&lt;/p&gt;
+<?xml-stylesheet type="text/xsl" href="../assets/xml/rss.xsl" media="all"?><rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Lean community blog (Posts by Emily Riehl)</title><link>https://leanprover-community.github.io/blog/</link><description></description><atom:link href="https://leanprover-community.github.io/blog/authors/emily-riehl.xml" rel="self" type="application/rss+xml"></atom:link><language>en</language><copyright>Contents © 2024 &lt;a href="mailto:"&gt;The Lean prover community&lt;/a&gt; </copyright><lastBuildDate>Mon, 25 Nov 2024 17:49:59 GMT</lastBuildDate><generator>Nikola (getnikola.com)</generator><docs>http://blogs.law.harvard.edu/tech/rss</docs><item><title>Announcing the ∞-Cosmos Project</title><link>https://leanprover-community.github.io/blog/posts/infinity-cosmos-announcement/</link><dc:creator>Emily Riehl</dc:creator><description>&lt;div&gt;&lt;p&gt;&lt;a href="https://github.com/emilyriehl"&gt;Emily Riehl&lt;/a&gt; introduces the &lt;a href="https://github.com/emilyriehl/infinity-cosmos"&gt;∞-Cosmos Project&lt;/a&gt;.&lt;/p&gt;
 &lt;p&gt;&lt;a href="https://leanprover-community.github.io/blog/posts/infinity-cosmos-announcement/"&gt;Read more…&lt;/a&gt; (2 min remaining to read)&lt;/p&gt;&lt;/div&gt;</description><category>∞-Cosmos</category><guid>https://leanprover-community.github.io/blog/posts/infinity-cosmos-announcement/</guid><pubDate>Tue, 17 Sep 2024 18:00:00 GMT</pubDate></item></channel></rss>

docs/authors/frederic-dupuis.xml

@@ -1,3 +1,3 @@
 <?xml version="1.0" encoding="utf-8"?>
-<?xml-stylesheet type="text/xsl" href="../assets/xml/rss.xsl" media="all"?><rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Lean community blog (Posts by Frédéric Dupuis)</title><link>https://leanprover-community.github.io/blog/</link><description></description><atom:link href="https://leanprover-community.github.io/blog/authors/frederic-dupuis.xml" rel="self" type="application/rss+xml"></atom:link><language>en</language><copyright>Contents © 2024 &lt;a href="mailto:"&gt;The Lean prover community&lt;/a&gt; </copyright><lastBuildDate>Fri, 18 Oct 2024 08:28:43 GMT</lastBuildDate><generator>Nikola (getnikola.com)</generator><docs>http://blogs.law.harvard.edu/tech/rss</docs><item><title>Semilinear maps</title><link>https://leanprover-community.github.io/blog/posts/semilinear-maps/</link><dc:creator>Frédéric Dupuis</dc:creator><description>&lt;div&gt;&lt;p&gt;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.&lt;/p&gt;
+<?xml-stylesheet type="text/xsl" href="../assets/xml/rss.xsl" media="all"?><rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Lean community blog (Posts by Frédéric Dupuis)</title><link>https://leanprover-community.github.io/blog/</link><description></description><atom:link href="https://leanprover-community.github.io/blog/authors/frederic-dupuis.xml" rel="self" type="application/rss+xml"></atom:link><language>en</language><copyright>Contents © 2024 &lt;a href="mailto:"&gt;The Lean prover community&lt;/a&gt; </copyright><lastBuildDate>Mon, 25 Nov 2024 17:49:59 GMT</lastBuildDate><generator>Nikola (getnikola.com)</generator><docs>http://blogs.law.harvard.edu/tech/rss</docs><item><title>Semilinear maps</title><link>https://leanprover-community.github.io/blog/posts/semilinear-maps/</link><dc:creator>Frédéric Dupuis</dc:creator><description>&lt;div&gt;&lt;p&gt;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.&lt;/p&gt;
 &lt;p&gt;&lt;a href="https://leanprover-community.github.io/blog/posts/semilinear-maps/"&gt;Read more…&lt;/a&gt; (4 min remaining to read)&lt;/p&gt;&lt;/div&gt;</description><guid>https://leanprover-community.github.io/blog/posts/semilinear-maps/</guid><pubDate>Sat, 11 Dec 2021 11:00:00 GMT</pubDate></item></channel></rss>