deploy site from 8184b19

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-09-17T18:00:00Z" title="2024-09-17 18:00">2024-09-17 18:00</time><a href="../posts/infinity-cosmos-announcement/" class="listtitle">Announcing the ∞-Cosmos Project</a>
+</li>
+        <li>
 <time class="listdate" datetime="2024-07-01T12:00:00Z" title="2024-07-01 12:00">2024-07-01 12:00</time><a href="../posts/month-in-mathlib/2024/month-in-mathlib-may-2024/" class="listtitle">This month in Mathlib (May 2024)</a>
 </li>
         <li>

docs/archive.html

@@ -44,7 +44,7 @@
     </header><ul class="postlist">
 <li>
 <a href="2024/">2024</a>
-            (2)
+            (3)
         </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, 02 Aug 2024 16:48:21 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>Wed, 18 Sep 2024 00:13: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).
 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, 02 Aug 2024 16:48:21 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>Wed, 18 Sep 2024 00:13: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).
 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, 02 Aug 2024 16:48:22 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>Wed, 18 Sep 2024 00:13: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;
 &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, 02 Aug 2024 16:48:21 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>Wed, 18 Sep 2024 00:13: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;
 &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

@@ -0,0 +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>Wed, 18 Sep 2024 00:13: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;
+&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/emily-riehl/index.html

@@ -0,0 +1,65 @@
+<!DOCTYPE html>
+<html prefix="
+og: http://ogp.me/ns# article: http://ogp.me/ns/article#
+" lang="en">
+<head>
+<meta charset="utf-8">
+<meta name="viewport" content="width=device-width, initial-scale=1">
+<title>Posts by Emily Riehl | Lean community blog</title>
+<link href="../../assets/css/rst.css" rel="stylesheet" type="text/css">
+<link href="../../assets/css/code.css" rel="stylesheet" type="text/css">
+<link href="../../assets/css/theme.css" rel="stylesheet" type="text/css">
+<link href="../../assets/css/custom.css" rel="stylesheet" type="text/css">
+<link href="https://fonts.googleapis.com/css2?family=Merriweather&amp;family=Open+Sans&amp;family=Source+Code+Pro:wght@400;600&amp;display=swap" rel="stylesheet">
+<meta name="theme-color" content="#5670d4">
+<meta name="generator" content="Nikola (getnikola.com)">
+<link rel="alternate" type="application/rss+xml" title="RSS" hreflang="en" href="../../rss.xml">
+<link rel="canonical" href="https://leanprover-community.github.io/blog/authors/emily-riehl/">
+<link rel="icon" href="https://leanprover-community.github.io/img/favicon.ico" sizes="48x48">
+<!--[if lt IE 9]><script src="../../assets/js/html5.js"></script><![endif]--><meta name="twitter:card" content="summary">
+<meta name="twitter:image" content="https://leanprover-community.github.io/blog/meta-twitter.png">
+<meta name="twitter:title" content="Posts by Emily Riehl | Lean community blog">
+<link rel="alternate" type="application/rss+xml" title="RSS for author Emily Riehl" hreflang="en" href="../emily-riehl.xml">
+</head>
+<body>
+    <a href="#content" class="sr-only sr-only-focusable">Skip to main content</a>
+    <div id="container">
+            <header id="header"><h1 id="brand"><a href="../../" title="Lean community blog" rel="home">
+
+        <span id="blog-title">Lean community blog</span>
+    </a></h1>
+
+
+            <nav id="menu"><ul>
+<li><a href="https://leanprover-community.github.io/">Main site</a></li>
+                <li><a href="../../archive.html">Archive</a></li>
+                <li><a href="../../categories/">Tags</a></li>
+                <li><a href="../../about/">About</a></li>
+                <li><a href="../../rss.xml">RSS feed</a></li>
+
+
+
+
+    </ul></nav></header><main id="content"><article class="authorpage"><header><h1>Posts by Emily Riehl</h1>
+        <div class="metadata">
+                            <p class="feedlink">
+                                    <a href="../emily-riehl.xml" hreflang="en" type="application/rss+xml">RSS feed</a>
+
+                </p>
+
+        </div>
+    </header><ul class="postlist">
+<li>
+<time class="listdate" datetime="2024-09-17T18:00:00Z" title="2024-09-17 18:00">2024-09-17 18:00</time><a href="../../posts/infinity-cosmos-announcement/" class="listtitle">Announcing the ∞-Cosmos Project</a>
+</li>
+        </ul></article><script src="https://giscus.app/client.js" data-repo="leanprover-community/blog" data-repo-id="MDEwOlJlcG9zaXRvcnkzOTM3OTE1ODU=" data-category="Announcements" data-category-id="DIC_kwDOF3jIYc4CQntU" data-mapping="og:title" data-strict="1" data-reactions-enabled="1" data-emit-metadata="0" data-input-position="bottom" data-theme="light" data-lang="en" crossorigin="anonymous" async>
+        </script></main><footer id="footer"><p>Contents © 2024         The Lean prover community - Powered by         <a href="https://getnikola.com" rel="nofollow">Nikola</a>         </p>
+
+        </footer>
+</div>
+
+
+
+
+</body>
+</html>