Math Blog

Rubik’s Cube in Lean

lean

This Github repo contains the proof that there are \(2^{12} \times 3^{8} \times 8! \times 11!\) Rubik’s cubes.

Mir Publications

textbooks

russian

I loathe American textbooks from the bottom of my heart. I learned math from these tiny 100 page books that made the point…

Pythagoras using Hilbert 90

abstract algebra

Dummit and Foote has a fun way of classifying Pythagorean triples. It is a classic fact that if \((a, b, c)\) is a reduced Pythagorean triple then there exists integers \…

Phistomephel Ring in Sudoku

sudoku

Came across this really cool short video about identities in a Sudoku square:

Closed Convex Cones in LP

analysis

linear programming

convex analysis

I was formalizing some linear programming in Lean and came across one of the most surprisingly difficult to prove theorems.

Combinatorial Nullstellensatz

combinatorics

problems

todo

I came across this fun theorem in a talk about tree colorings:

Terrence Tao - Lean

lean

mathblog

Terry Tao posted on Mastodon that he found a bug in a proof in one of his papers thanks to trying to formalize it in Lean. This is an…

PaperProof

lean

vscode extension

visualization

teaching

This looks like a really cool tool for visualizing proofs in Lean:

Logarithms and primes

todo

infinite series

number theory

riemann zeta

I came across this video by NumberPhile and 3Blue1Brown about the density of primes that are 1 mod 4 vs the density of…

How They Fool Ya (live) | Math parody of Hallelujah

funny

The Tau Manifesto

funny

database

\(\tau\) manifesto

The L-functions and modular forms database (LMFDB)

database

number theory

Automated Mathematics and the Reconfiguration of Proof and Labor

to-read

philosophy

essay

I came across this essay by Rodrigo Ochigame exploring possible future impact of math formalization and automation.

When Math Becomes an Art

poem

A post shared by Elle Cordova (@ellecordova)

Every Prime \(\equiv 1 \mod 4\) Is a Sum of Two Squares

todo

number theory

elementary number theory

I came across this “one sentence” proof that every prime congruent to 1 mod 4 can be written as a sum of two squares:

llmstep and LeanInfer

lean

ML

tactics

I came across two LLM based tactics for Lean

LeanDojo

lean

ML

webapp

This was posted a while back on the Lean Zulip:

Short tactics tutorial

lean

tactics

tutorial

to-read

I have always wanted to learn tactics writing in Lean. But for whatever reason, none of the tutorials that exist online have been helpful. I suspect that the best way to…

Loogle!

lean

search

webapp

An improved search engine for Lean:

Etymology of Integer

history of math

We use integers so much in math that it never occurred to me before yesterday that this is a weird word with a weirder symbol associated to it. Wikipedia exp…

History-of-Math Resources

resources

history of math

I’ve always been fascinated by the history of mathematics. Some of the classic and dramatic discoveries I read a kid were those of non-Euclidean geometry, Galois theory, the…