Here’s a round-up of some news from the last couple of months.
You're reading: Posts Tagged: Lean
Double Maths First Thing: Issue 30
Double Maths First Thing keeps getting bumped to the next room
Hello! My name is Colin and I am a mathematician on a mission to spread delight and joy in mathematical thinking and practice.
This week, the kids are at a sailing course. I’ve never quite understood how it’s possible to sail into the wind, so I’m looking forward to them explaining this to me.
Links
A nice puzzle via Mair in the Finite Group discord: you have a triangle with an obtuse angle, and need to divide it into triangles with only acute angles. How many triangles do you need?
At the brilliantly-titled Solutions Looking For Problems blog, Bryan Wolf wondered if there’s a ‘most-scrambled’ Rubik’s cube.
Here’s a thing of beauty: an alternative representation of the periodic table. There’s a wonderful collection of similar things at All Periodic Tables.
Also lovely: Christian Lawson-Perfect has implemented a simulation of a glass sudoku, in which cells move between energy states.
I haven’t put any time at all into examining the content of The Journal of Humanistic Mathematics, but at first glance it looks like an excellent project.
Lastly for this week, an overview of some of the things you can do in Lean, including making the maths haunted.
Currently
There’s a new Carnival of Maths, courtesy of Katie at the Aperiodical. I’m hosting the next one, and you can submit links here.
The TMiP animation challenge for July has closed, with a playlist of responses here. August’s challenge is Hilbert curves, which is always a good excuse to mention the flowsnake — and to point out that the next Finite Group livestream is on space-filling curves.
That’s all I’ve got for this week. If you have friends and/or colleagues who would enjoy Double Maths First Thing, do send them the link to sign up — they’ll be very welcome here.
If you’ve missed the previous issues of DMFT or — somehow — this one, you can find the archive courtesy of my dear friends at the Aperiodical.
Meanwhile, if there’s something I should know about, you can find me on Mathstodon as @icecolbeveridge, or at my personal website. You can also just reply to this email if there’s something you want to tell me.
Until next time,
C
Aperiodical News Roundup – July 2023
Here’s some mathematical news that didn’t make it on to the site otherwise this month.
Maths News
There’s been more abc conjecture drama: Peter Scholze and Jakob Stix are in line for a ¥140m (around £766k) prize for their paper pointing out the flaw in Mochizuki’s claimed abc proof – if they publish it in a journal.
A period 19 oscillator has been found in Conway’s game of life – the discussion thread on ConwayLife just gives it as a series of coordinates, but it already has an entry on LifeWiki, where it’s called ‘Cribbage’. (via Isaac Grosof)
Then, a week later, the first ever period 41 oscillator was also found! Excitingly named 204P41 (consisting of 204 cells) it’s led to another discovery – it looks like we now know how to make oscillators with any period, meaning Game of Life is omniperiodic. Since 2013 we’ve known all periods above 43 were possible, and this fills a gap in this excellent table.
Lean’s mathlib has been completely ported to Lean4 – if you’re familiar with proof assistants, you may find this news exciting or significant. Here’s a video showing off what that looks like. Meanwhile, the Lean Focused Research Organization has been set up to “advance the formal mathematics revolution”. (via @leanprover@functional.cafe)
Events and Organisations
Inclusion/Exclusion, a justice and maths blog, has posted an open letter to the MAA about holding MathFest in Florida, requesting an option for online participation due to the state’s recent draconian law changes. It pulls ε punches:
Regardless of any in-person safeguards that MAA may put in place, this year’s MathFest will not be a safe event for trans people, for undocumented immigrants, or for many other members of our community, including disabled people. Therefore, our most urgent request is that you provide an online participation option.
Excerpt from the open letter
If π approximation day on 22/7 got you thinking about your plans for the next actual π day, you might find it useful to know that the International Day of Mathematics 2024 theme is Playing With Math. From their website, “In 2024 we want to celebrate mathematical games, puzzles and other entertaining activities, but also “playing” with mathematics itself, exploring, experimenting, and discovering.”
Speaking of mathematical games, Ben Orlin has released a book of solitaire games as a follow-up to his “Math Games with Bad Drawings”. It’s available for free on his website as a PDF, and therefore weighs infinity less than the actual book it’s a follow-up to, which is so huge it’s collapsed into a black hole under its own mass. (via Patrick Honner)
And finally: Tim Wall, the Australian group theorist, has died. According to his profile on the Australian Academy of Science website, Wall “has made highly significant and original contributions to the development of Algebra, in particular to the Theory of Groups. […] He has always instinctingly given of his ideas to his collaborators and younger colleagues.” Thanks Tim!
Aperiodical News Roundup – October 2022
Research
AI research company DeepMind said that their AlphaTensor system has discovered a new way to multiply matrices, citing this as the first such advance since the Strassen algorithm was proposed in 1969. AlphaTensor found thousands of algorithms for multiplying matrices of different sizes, but most were not better than the state of the art. Specifically, it found an algorithm for multiplying \(5 \times 5\) matrices in \(\mathbb{Z}_2\) in just 96 operations. There’s a paper in Nature describing how the algorithm was found.
It’s not all over for us humans just yet, though: the DeepMind announcement prompted two algebraists at Linz University, Jakob Moosbauer and Manuel Kauers, to see if they could do even better. After a few days of thought, they published The FBHHRBNRSSSHK-Algorithm for Multiplication in $\mathbb{Z}_2^{5\times5}$ is still not the end of the story on the arXiv, giving an algorithm which does the multiplication in only 95 steps.
Meanwhile, in other computers-helping-humans news, the Lean 3 library mathlib has made it to 100,000 theorems, none of which have been left as an exercise for the reader.
Events
The IMA and LMS have joined forces to offer a new university access programme called Levelling Up: Maths, which aims to address the difficulties that young people of Black heritage face in STEM. A-level students can join the programme, and will be able to access teaching and mentoring in virtual tutorial groups with Black heritage undergraduates, as well as events with Black guest speakers. The programme is also supported by the RAEng, BCS, IOP RSC, MEI and STEM Learning, as well as the Association for Black & Minority Ethnic Engineers (AFBE-UK) and Black British Professionals in STEM (BBSTEM).
What Can Mathematicians Do? is a series of free online public maths presentations organised by Newcastle University’s School of Mathematics, Statistics and Physics, covering a wide range of topics such as how colours mix, how to make a mint on the stock market, and how to pick your next Netflix binge. Aimed at students in school years 10 to 13, the talks are all given by disabled presenters: to show that anyone can be a mathematician, and mathematicians can do anything.
And finally: last weekend, a group of maths communicators (including several Aperiodical editors and regulars) put together a live online 24-hour Mathematical Game Show, featuring mathematical games, games with a mathematical twist, the maths of games and games about maths. The show has raised nearly £5000 for a collection of excellent charities, and the whole show is available to watch back in half-hour or 1-hour segments.
And finally
Nick Berry of the Data Genetics blog has died. The site ran for over a decade, and was described by Alex Bellos as ‘one of best examples of maths outreach on the web […] A brilliant cabinet of curiosities’. Nick passed away peacefully at home on Saturday October 8th after a long battle with cancer. (via Alex Bellos on Twitter)
Phil Goldstein, aka magician Max Maven, has died. Max Maven popularised the Gilbreath principle, which underlies a host of astonishing mathematical card tricks. (via Colm Mulcahy on Twitter)
Aperiodical News Roundup – July 2022
Here’s a roundup of some mathematical news we didn’t yet report from the last month.
The makers of documentary film ‘Olga Ladyzhenskaya’, detailing the life of the Russian mathematician, have released a five-minute trailer giving a flavour of the film. (via ICM Intelligencer)
Research
According to a new ArXiV paper, the triple bubble conjecture (a result about the shapes taken by surfaces that are attempting to enclose a volume, or in this case three volumes, with minimal surface area) has been solved. (via Ian Agol)
The Lean community, who use and blog about the Lean proof assistant, have announced completion of the liquid tensor experiment – proving the main theorem of liquid vector spaces (me neither) and thereby formalising a big serious proof using the system. (via David Eppstein)
In computer science, a new ArXiV paper takes us a step closer to automating quantitative reasoning – Minerva, a large language model pre-trained on general natural language data and technical content, has correctly solved some college-level questions that “require quantitative reasoning”.
Awards
A big month for prizes, with the announcement of the 2022 Fields medals, awarded to Hugo Duminil-Copin, June Huh, James Maynard and Maryna Viazovska, as well as the 2022 Christopher Zeeman medal, which has been awarded to Simon Singh.
Aperiodical News Roundup – January 2022
Here’s a roundup of some of the mathematical things that happened in the first month of the year.