Owen Maresh

https://arxiv.org/abs/2604.23468
/A Milestone in Formalization: The Sphere Packing Problem in Dimension 8/
Sidharth Hariharan, Christopher Birkbeck, Seewoo Lee, Ho Kiu Gareth Ma, Bhavik Mehta, Auguste Poiroux, Maryna Viazovska

abstract:
In 2016, Viazovska famously solved the sphere packing problem in dimension 8, using modular forms to construct a 'magic' function satisfying optimality conditions determined by Cohn and Elkies in 2003. In March 2024, Hariharan and Viazovska launched a project to formalize this solution and related mathematical facts in the Lean Theorem Prover. A significant milestone was achieved in February 2026: the result was formally verified, with the final stages of the verification done by Math, Inc.'s autoformalization model 'Gauss'. We discuss the techniques used to achieve this milestone, reflect on the unique collaboration between humans and Gauss, and discuss project objectives that remain.

What is the relationship between slitscan -- a filmmaking technique used for the Stargate sequence in Stanley Kubrick's 2001, the going to hyperspace effect in SW, the dopplered star effect in Trek -- and Morse Theory?

https://en.wikipedia.org/wiki/Morse_theory

https://www.youtube.com/watch?v=qKOAOzVHvFQ&t=1157s
/VFX History: Slit Scan/ by
ShiveringCactus: VFX

from the video description:

How did 2001: A Space Odyssey, Star Wars, Doctor Who and Star Trek: The Next Generation create mind-bending visuals decades before CGI?
The secret is Slitscan, a terrifyingly complex technique that literally turns time into space.

In this deep dive into VFX history, I explore the origins of the Slitscan technique. From its humble beginnings in 19th-century "strip photography" used for horse racing and mapping, to the genius of John Whitney and Douglas Trumbull, we look at how a mechanical slit, a long-exposure camera, and patience created the most iconic "trippy" visuals in cinema.

In the late 1990s I was working through organizing some of my writing and rearranging the order was done in the bookmarks editor of netscape on an SGI O2...

About the only decent modern equivalent seems like Omnioutliner. (org-mode?, eek).

It would be swell if the slew of paper with (gradient descent combine)-named sections and subsections would stop, or at least be mollified in some way: being able to have more fine grained control of sectioning and subsection, preferable through a gui, might have some damping effect.

odd question: for the Borwein cubic theta functions, and for the Jacobian theta functions satisfying a fourth power identity... is there a Frey curve?

https://www.youtube.com/watch?v=4MQbd5wTlI8

Emily Riehl (@emilyriehl@mathstodon.xyz ) Higher Category Theory, Homotopy & AI in Math | aboutlogic #15

(from the video description):
------
aboutlogic #15 | Emily Riehl (Johns Hopkins University) joins us to explore higher category theory, homotopy, and the role of AI in modern mathematics. From the foundations of category theory to the challenges of formalizing math with proof assistants like Lean, Emily shares her insights on synthetic vs. analytic approaches, the beauty of abstraction, and how AI is changing mathematical research.

Listen to the podcast on the go: https://aboutlogic.podigee.io/

00:50 Introduction to Higher Category Theory
02:37 Understanding Homotopy Theory
09:44 Exploring Category Theory Basics
15:52 Limitations and Complexities in Category Theory
21:58 The Role of Proof Assistants in Category Theory
27:59 Synthetic vs Analytic Approaches in Infinity Categories
36:33 Teaching and Learning with Proof Assistants and the use of AI
48:40 Gender Imbalance in Mathematics
51:43 Bridging the Gap Between Type Theory and Set Theory

Get the HoTT Book for free (no advertisement): https://homotopytypetheory.org/book/
Thorsten Altenkirch: http://www.cs.nott.ac.uk/~psztxa/
Deniz Sarikaya: https://www.denizsarikaya.de/
Creative Production: Jan-Niklas Meyer: http://www.jammos.com/

------