Math Blog

Math Arena AI

lean

AI

LLM

I was doing some research for a talk and came across this website for recording AI results on math problems: https://matharena.ai/

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 directly and succinctly and trusted the reader’s…

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 \(m…

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 excellent use case of Lean and tbh the…

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 primes that are 3 mod 4. The main fact is quite cool…

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 explains this very…

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…