-
Notifications
You must be signed in to change notification settings - Fork 20
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
623bd87
commit 9e67dcf
Showing
35 changed files
with
151 additions
and
151 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 <a href="mailto:">The Lean prover community</a> </copyright><lastBuildDate>Mon, 01 Jul 2024 21:39:41 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><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> | ||
<?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 <a href="mailto:">The Lean prover community</a> </copyright><lastBuildDate>Tue, 02 Jul 2024 16:42:36 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><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></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> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 <a href="mailto:">The Lean prover community</a> </copyright><lastBuildDate>Mon, 01 Jul 2024 21:39:41 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><div><p><img alt="mathlib-changelog sample page" src="https://leanprover-community.github.io/blog/images/changelog_lemma.png"></p> | ||
<?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 <a href="mailto:">The Lean prover community</a> </copyright><lastBuildDate>Tue, 02 Jul 2024 16:42:36 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><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></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> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 <a href="mailto:">The Lean prover community</a> </copyright><lastBuildDate>Mon, 01 Jul 2024 21:39:41 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><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> | ||
<?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 <a href="mailto:">The Lean prover community</a> </copyright><lastBuildDate>Tue, 02 Jul 2024 16:42:36 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><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></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> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.