Brouwer's fixed point theorem in Lean 4
There are several kinds of proofs for Brouwer's fixed point theorem. Nnevertheless, currently the theorem seems not part of Mathlib4.
Yet, we have seen some attempting its formal proof in Lean 4. For example, harfe/fixed-point-theorems-lean4 has done successfully by formalizing and relying on cubical Sperner's Lemma.
Today we asked Harmonics's Aristotle to prove the following variant of the theorem:
Every continuous function from a nonempty convex compact subset K of a Euclidean space to K itself has a fixed point.
Then the AI agent used the No-retraction theorem to get things done: shared link.
Archives
2026-08-17: A colouring argument in Lean 4
2026-08-07: The Sylvester-Gallai theorem in Lean 4
2026-05-13: Minasp v0.6.11 released for Mew v6.11
2024-04-11: Running Torch for R with CUDA in a Docker container
2024-03-17: Introducing Minasp, a Nix package of Mew
2024-03-02: How to view a figure plotted by Plotly R from macOS Terminal
2024-02-20: How to cite references in Org Mode with Zotero
2024-02-18: Heads up for endangered "404 Not Found" pages
2024-02-17: Finding another blog about Nix: Nixcademy
2024-02-12: Writing blog articles with Org Mode
2023: Jan | Feb | Mar | Apr | May | Jun | Jul | Aug | Sep | Oct | Nov | Dec
2022: Jan | Feb | Mar | Apr | May | Jun | Jul | Aug | Sep | Oct | Nov | Dec
2021: Jan | Feb | Mar | Apr | May | Jun | Jul | Aug | Sep | Oct | Nov | Dec
2020: Jan | Feb | Mar | Apr | May | Jun | Jul | Aug | Sep | Oct | Nov | Dec
2019: Jan | Feb | Mar | Apr | May | Jun | Jul | Aug | Sep | Oct | Nov | Dec
2018: Jan | Feb | Mar | Apr | May | Jun | Jul | Aug | Sep | Oct | Nov | Dec
2017: Jan | Feb | Mar | Apr | May | Jun | Jul | Aug | Sep | Oct | Nov | Dec
2016: Jan | Feb | Mar | Apr | May | Jun | Jul | Aug | Sep | Oct | Nov | Dec
2015: Jan | Feb | Mar | Apr | May | Jun | Jul | Aug | Sep | Oct | Nov | Dec
2014: Jan | Feb | Mar | Apr | May | Jun | Jul | Aug | Sep | Oct | Nov | Dec
2013: Jan | Feb | Mar | Apr | May | Jun | Jul | Aug | Sep | Oct | Nov | Dec
2012: Jan | Feb | Mar | Apr | May | Jun | Jul | Aug | Sep | Oct | Nov | Dec
2011: Jan | Feb | Mar | Apr | May | Jun | Jul | Aug | Sep | Oct | Nov | Dec
2010: Jan | Feb | Mar | Apr | May | Jun | Jul | Aug | Sep | Oct | Nov | Dec
2009: Jan | Feb | Mar | Apr | May | Jun | Jul | Aug | Sep | Oct | Nov | Dec
2008: Jan | Feb | Mar | Apr | May | Jun | Jul | Aug | Sep | Oct | Nov | Dec
2007: Jan | Feb | Mar | Apr | May | Jun | Jul | Aug | Sep | Oct | Nov | Dec
2006: Jan | Feb | Mar | Apr | May | Jun | Jul | Aug | Sep | Oct | Nov | Dec