You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
<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>
<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>
4
4
<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>
<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>
a more abstract concept which, importantly, unifies linear and conjugate-linear maps.</p>
4
4
<p>But this is not the full extent of the generalization! Our number theorist friends here in mathlib told us that we should
5
5
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>
The workshop took place in Leiden from July 10th to July 14th 2023, and it was an amazing and educational journey.</p>
4
4
<p><a href="https://leanprover-community.github.io/blog/posts/lorentz-center-meeting/">Read more…</a> (4 min remaining to read)</p></div></description><guid>https://leanprover-community.github.io/blog/posts/lorentz-center-meeting/</guid><pubDate>Sat, 26 Aug 2023 14:30:00 GMT</pubDate></item></channel></rss>
from blockchain entrepreneur Charles C. Hoskinson will be used to establish the Hoskinson
4
4
Center for Formal Mathematics, housed in the Department of Philosophy.
5
5
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
<p><a href="https://leanprover-community.github.io/blog/posts/FLT-announcement/">Read more…</a> (5 min remaining to read)</p></div></description><guid>https://leanprover-community.github.io/blog/posts/FLT-announcement/</guid><pubDate>Tue, 30 Apr 2024 18:00:00 GMT</pubDate></item><item><title>Formalising cohomology theories</title><link>https://leanprover-community.github.io/blog/posts/banff-cohomology/</link><dc:creator>Kevin Buzzard</dc:creator><description><div><p>Kevin Buzzard rounds up the BIRS conference on formalising cohomology theories.</p>
4
4
<p><a href="https://leanprover-community.github.io/blog/posts/banff-cohomology/">Read more…</a> (6 min remaining to read)</p></div></description><guid>https://leanprover-community.github.io/blog/posts/banff-cohomology/</guid><pubDate>Mon, 12 Jun 2023 07:42:45 GMT</pubDate></item></channel></rss>
<p>There were 667 PRs merged in May 2024.</p>
4
4
<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></description><guid>https://leanprover-community.github.io/blog/posts/month-in-mathlib/2024/month-in-mathlib-may-2024/</guid><pubDate>Mon, 01 Jul 2024 12:00:00 GMT</pubDate></item><item><title>This month in mathlib (Sep 2022)</title><link>https://leanprover-community.github.io/blog/posts/month-in-mathlib/2022/month-in-mathlib-sep-2022/</link><dc:creator>Mathlib community</dc:creator><description><div><p>In September 2022 there were 361 PRs merged into mathlib. We list some of the highlights below.</p>
5
5
<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></description><guid>https://leanprover-community.github.io/blog/posts/month-in-mathlib/2022/month-in-mathlib-sep-2022/</guid><pubDate>Sat, 08 Oct 2022 06:01:27 GMT</pubDate></item><item><title>This month in mathlib (Aug 2022)</title><link>https://leanprover-community.github.io/blog/posts/month-in-mathlib/2022/month-in-mathlib-aug-2022/</link><dc:creator>Mathlib community</dc:creator><description><div><p>In August 2022 there were 506 PRs merged into mathlib. We list some of the highlights below.</p>
a more abstract concept which, importantly, unifies linear and conjugate-linear maps.</p>
4
4
<p>But this is not the full extent of the generalization! Our number theorist friends here in mathlib told us that we should
5
5
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>
We're excited to transition from only providing nightly releases to having regular stable releases.</p>
4
4
<p><a href="https://leanprover-community.github.io/blog/posts/first-lean-release/">Read more…</a> (1 min remaining to read)</p></div></description><guid>https://leanprover-community.github.io/blog/posts/first-lean-release/</guid><pubDate>Fri, 08 Sep 2023 05:58:40 GMT</pubDate></item><item><title>Update on mathport (Dec 2021)</title><link>https://leanprover-community.github.io/blog/posts/intro-to-mathport/</link><dc:creator>Scott Morrison</dc:creator><description><div><p><code>mathport</code> is the tool we're planning on using to help us port <code>mathlib</code> to Lean 4.
5
5
It has mostly been written by Mario Carneiro and Daniel Selsam,
from blockchain entrepreneur Charles C. Hoskinson will be used to establish the Hoskinson
4
4
Center for Formal Mathematics, housed in the Department of Philosophy.
5
5
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
The workshop took place in Leiden from July 10th to July 14th 2023, and it was an amazing and educational journey.</p>
4
4
<p><a href="https://leanprover-community.github.io/blog/posts/lorentz-center-meeting/">Read more…</a> (4 min remaining to read)</p></div></description><guid>https://leanprover-community.github.io/blog/posts/lorentz-center-meeting/</guid><pubDate>Sat, 26 Aug 2023 14:30:00 GMT</pubDate></item><item><title>Formalising cohomology theories</title><link>https://leanprover-community.github.io/blog/posts/banff-cohomology/</link><dc:creator>Kevin Buzzard</dc:creator><description><div><p>Kevin Buzzard rounds up the BIRS conference on formalising cohomology theories.</p>
5
5
<p><a href="https://leanprover-community.github.io/blog/posts/banff-cohomology/">Read more…</a> (6 min remaining to read)</p></div></description><guid>https://leanprover-community.github.io/blog/posts/banff-cohomology/</guid><pubDate>Mon, 12 Jun 2023 07:42:45 GMT</pubDate></item></channel></rss>
<p>There were 667 PRs merged in May 2024.</p>
4
4
<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></description><guid>https://leanprover-community.github.io/blog/posts/month-in-mathlib/2024/month-in-mathlib-may-2024/</guid><pubDate>Mon, 01 Jul 2024 12:00:00 GMT</pubDate></item><item><title>This month in mathlib (Oct and Nov 2022)</title><link>https://leanprover-community.github.io/blog/posts/month-in-mathlib/2022/month-in-mathlib-oct-and-nov-2022/</link><dc:creator>The Lean prover community</dc:creator><description><div><p>In October and November 2022 there were 512 and 453 PRs merged into mathlib. We list some of the highlights below.</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><item><title>Classification of one-dimensional isocrystals</title><link>https://leanprover-community.github.io/blog/posts/classification-of-one-dimensional-isocrystals/</link><dc:creator>Robert Y. Lewis, Heather Macbeth</dc:creator><description><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>,
4
4
a more abstract concept which, importantly, unifies linear and conjugate-linear maps.</p>
5
5
<p>But this is not the full extent of the generalization! Our number theorist friends here in mathlib told us that we should
As an end-of-year retrospective, we look at how the mathlib library and community have developed in 2021.</p>
5
5
<p><a href="https://leanprover-community.github.io/blog/posts/2021-the-bottom-line/">Read more…</a> (5 min remaining to read)</p></div></description><guid>https://leanprover-community.github.io/blog/posts/2021-the-bottom-line/</guid><pubDate>Sat, 08 Jan 2022 19:35:59 GMT</pubDate></item></channel></rss>
Copy file name to clipboardExpand all lines: docs/posts/month-in-mathlib/2024/month-in-mathlib-may-2024/index.html
+5-3Lines changed: 5 additions & 3 deletions
Original file line number
Diff line number
Diff line change
@@ -121,10 +121,12 @@
121
121
<ahref="https://github.com/leanprover-community/mathlib4/pull/12701">PR #12701</a> redefines sets without arithmetic progressions of length 3 (aka 3AP-free sets) so that they behave correctly in characteristic two. <ahref="https://github.com/leanprover-community/mathlib4/pull/12546">PR #12546</a> refactors Freiman homomorphisms and isomorphisms from a bundled design to unbundled predicates. This makes them much easier to use. <ahref="https://github.com/leanprover-community/mathlib4/pull/12551">PR #12551</a> then proves the no wrap-around principle stating that additive structure in sets is independent of the ambient group so long as torsion is much bigger than the diameter of the sets.</li>
122
122
<li>Building up on thoses two series of PRs, <ahref="https://github.com/leanprover-community/mathlib4/pull/13074">PR #13074</a> defines corners and corner-free set and <ahref="https://github.com/leanprover-community/mathlib4/pull/9000">PR #9000</a> finally proves the Corners theorem and Roth's theorem. They respectively state that a corner-free set in <code>[N] × [N]</code> and a 3AP-free set in <code>[N]</code> have vanishingly small density as <code>N</code> goes to infinity.</li>
123
123
</ul>
124
-
<p><ahref="https://github.com/YaelDillies/LeanAPAP">APAP</a> already contains the stronger result that the density goes to zero as <code>1/log log N</code>, and will soon prove the state of the art bound of <code>exp(-(log N)^1/9)</code>.
125
-
* <ahref="https://github.com/leanprover-community/mathlib4/pull/10555">PR #10555</a> defines dissociation of sets, a sort of "local" version of linear independence obtained by restricting the scalars to <code>{-1, 0, 1}</code>. This will soon be used to prove important results in additive combinatorics.
126
-
* Mathlib finally knows about Hamiltonian paths and cycles thanks to a team effort started at Lean for the Curious Mathematician 2023 in Düsseldorf by Rishi Mehta and Linus Sommer under the supervision of Bhavik Mehta, and recently continued by Lode Vermeulen in <ahref="https://github.com/leanprover-community/mathlib4/pull/7102">PR #7102</a>.</p>
124
+
<p><ahref="https://github.com/YaelDillies/LeanAPAP">APAP</a> already contains the stronger result that the density goes to zero as <code>1/log log N</code>, and will soon prove the state of the art bound of <code>exp(-(log N)^1/9)</code>.</p>
127
125
</li>
126
+
<li>
127
+
<p><ahref="https://github.com/leanprover-community/mathlib4/pull/10555">PR #10555</a> defines dissociation of sets, a sort of "local" version of linear independence obtained by restricting the scalars to <code>{-1, 0, 1}</code>. This will soon be used to prove important results in additive combinatorics.</p>
128
+
</li>
129
+
<li>Mathlib finally knows about Hamiltonian paths and cycles thanks to a team effort started at Lean for the Curious Mathematician 2023 in Düsseldorf by Rishi Mehta and Linus Sommer under the supervision of Bhavik Mehta, and recently continued by Lode Vermeulen in <ahref="https://github.com/leanprover-community/mathlib4/pull/7102">PR #7102</a>.</li>
Copy file name to clipboardExpand all lines: docs/posts/month-in-mathlib/2024/month-in-mathlib-may-2024/index.md
+2Lines changed: 2 additions & 0 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -46,11 +46,13 @@ There were 667 PRs merged in May 2024.
46
46
47
47
* Combinatorics.
48
48
* Thanks to the reviews by Thomas Bloom, a long sequence of three years old material by Yaël Dillies and Bhavik Mehta culminating in Roth's theorem on arithmetic progressions was finally merged:
49
+
49
50
* [PR #12526](https://github.com/leanprover-community/mathlib4/pull/12526) defines locally linear graphs, [PR #12570](https://github.com/leanprover-community/mathlib4/pull/12570) constructs such graphs from a set of specified triangles respecting some conditions, [PR #12523](https://github.com/leanprover-community/mathlib4/pull/12523) uses that construction to deduce the Triangle removal lemma from the Regularity lemma.
50
51
* [PR #12701](https://github.com/leanprover-community/mathlib4/pull/12701) redefines sets without arithmetic progressions of length 3 (aka 3AP-free sets) so that they behave correctly in characteristic two. [PR #12546](https://github.com/leanprover-community/mathlib4/pull/12546) refactors Freiman homomorphisms and isomorphisms from a bundled design to unbundled predicates. This makes them much easier to use. [PR #12551](https://github.com/leanprover-community/mathlib4/pull/12551) then proves the no wrap-around principle stating that additive structure in sets is independent of the ambient group so long as torsion is much bigger than the diameter of the sets.
51
52
* Building up on thoses two series of PRs, [PR #13074](https://github.com/leanprover-community/mathlib4/pull/13074) defines corners and corner-free set and [PR #9000](https://github.com/leanprover-community/mathlib4/pull/9000) finally proves the Corners theorem and Roth's theorem. They respectively state that a corner-free set in `[N] × [N]` and a 3AP-free set in `[N]` have vanishingly small density as `N` goes to infinity.
52
53
53
54
[APAP](https://github.com/YaelDillies/LeanAPAP) already contains the stronger result that the density goes to zero as `1/log log N`, and will soon prove the state of the art bound of `exp(-(log N)^1/9)`.
55
+
54
56
*[PR #10555](https://github.com/leanprover-community/mathlib4/pull/10555) defines dissociation of sets, a sort of "local" version of linear independence obtained by restricting the scalars to `{-1, 0, 1}`. This will soon be used to prove important results in additive combinatorics.
55
57
* Mathlib finally knows about Hamiltonian paths and cycles thanks to a team effort started at Lean for the Curious Mathematician 2023 in Düsseldorf by Rishi Mehta and Linus Sommer under the supervision of Bhavik Mehta, and recently continued by Lode Vermeulen in [PR #7102](https://github.com/leanprover-community/mathlib4/pull/7102).
<p>There were 667 PRs merged in May 2024.</p>
4
4
<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></description><guid>https://leanprover-community.github.io/blog/posts/month-in-mathlib/2024/month-in-mathlib-may-2024/</guid><pubDate>Mon, 01 Jul 2024 12:00:00 GMT</pubDate></item><item><title>The Fermat's Last Theorem Project</title><link>https://leanprover-community.github.io/blog/posts/FLT-announcement/</link><dc:creator>Kevin Buzzard</dc:creator><description><div><p>Kevin Buzzard discusses the project to prove Fermat's Last Theorem in Lean.</p>
5
5
<p><a href="https://leanprover-community.github.io/blog/posts/FLT-announcement/">Read more…</a> (5 min remaining to read)</p></div></description><guid>https://leanprover-community.github.io/blog/posts/FLT-announcement/</guid><pubDate>Tue, 30 Apr 2024 18:00:00 GMT</pubDate></item><item><title>The first official release of Lean 4</title><link>https://leanprover-community.github.io/blog/posts/first-lean-release/</link><dc:creator>Scott Morrison</dc:creator><description><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>.
0 commit comments