2026-06-25 10:38:42
I was reading an article this evening and saw a footnote to a book by Arthur Baragar [1]. This caught my eye because he was my officemate at UT for a year.
I found his book on Archive.org and was surprised to see “The Star Trek Lemma” in the table of contents. What could this be?
It’s a theorem that goes back to Euclid that applies to an angle formed by connecting a point to two other points on a circle. The theorem says “The measure of an inscribed angle is half the measure of the arc it subtends.” But why call it the Star Trek lemma? Quoting Arthur:
In the spirit of Euclid, we will refer to this theorem as the Star Trek lemma because of the figure associated with the statement of the theorem. … Before Star Trek, as far as I know, this theorem had no name, though some might call it Euclid III.20, which is its proposition number in Euclid’s Elements (Book III, Proposition 20).
Here is my reconstruction of the figure given in the book.
[1] Baragar, Arthur (2001), A Survey of Classical and Modern Geometries: With Computer Activities, Prentice Hall
The post The Star Trek lemma first appeared on John D. Cook.
2026-06-24 08:26:11
The most frustrating aspect of regular expressions is that implementations vary. Features supported in one tool may not be supported at all in another tool, or they may be supported with slightly different syntax.
I learned regular expressions in the context Perl, a maximalist regex environment. This led to frustration when features I expect to work are missing [1]. One way around this is to use Perl analogs of other tools, but this is very non-standard. I want to be able to send colleagues and clients code that works out of the box.
As I mentioned in my post on computational survivalism, I occasionally need to work on computers that I cannot install software on. So a better approach is to identify a subset of regex features that work everywhere. The stricter your definition of “everywhere” the less this includes. The strictest subset would be
[…]
. * ^ $
A more relaxed definition of “everywhere” would be the tools you most care about. Currently the tools I most want to use with regular expressions are sed, awk, grep, and Emacs.
If you use the Gnu versions of sed, awk, and grep, and use the -E option with sed and grep, then the list of common features is bigger. The regular expression features of of the three tools are similar, and awk’s features are supported in the other tools, with one exception: word boundaries in awk are \< and \> rather than \b and \B.
I wrote about Awk’s regex features here.
Emacs supports analogs of most of awk’s regex features. However, the characters
+ ? ( ) { } |
all require a backslash in front in order to act like the awk counterparts. Also, the analog of \s and \S in awk is \s- and \S- in Emacs.
Instead of meaning space or nonspace, \s and \S in Emacs begin a (negated) character class, and one of those classes is - for space. But there are many others. For example, \s. stands for a punctuation character and \S. stands for a non-punctuation character.
So for my definition of “everywhere,” with the caveats mentioned above, the following features work everywhere. YMMV.
.
^, $
[…], [^…]
*
\w, \W, \s, \S
\1 - \9 backreferences
\b \B
? +
| alternation
{n,m} for counting matches
(...) capturing
One footnote is that gawk supports backreferences in replacement strings but not in regular expressions per se.
[1] To some extent, basic Perl features work elsewhere and advanced features do not, depending on your idea of what is basic or advanced. I think of look-around features as advanced, and that tracks. But I think of \d for digits as basic, but that’s not supported in many regex flavors.
2026-06-23 04:02:47
Let f be an even function with period π. Then the following remarkable theorem by Lobachevsky holds.
This theorem is useful in Fourier analysis and signal processing. It’s useful to know even in the special case f(x) = 1.
For a “jinc” analog, see this paper.
***
Every time I see the name Lobachevsky I think of Tom Lehrer’s song about him. You can find the words here and the audio here.
2026-06-22 08:21:44
The n queens problem is to place on an n × n chessboard n queens so that none attacks any other. This means there is only one queen on every horizontal, vertical, and diagonal line.
When n is a prime number ≥ 5, it is sufficient to place the queens on a line that has slope 2, 3, 4, …, n − 2. (The slope cannot be 1 because that’s a diagonal. And it cannot be n − 1 because n − 1 = −1 mod n is also a diagonal.) [1]
Here we imagine opposite edges of the board being joined together. Geometrically, this makes the chessboard a torus (donut). Algebraically, the points on a line of slope s have the coordinates
(a + k, b + ks)
where addition is carried out mod n.
All solutions to the n queens problem have this form when n = 5. Some solutions will have this form for larger prime values of n but not all.
For example, when n = 7, here is a solution where all the queens are on a line of slope 2.
But here is another solution where the queens do not all lie on a line of constant slope.
[1] W. H. Bussey. A Note on the Problem of the Eight Queens. The American Mathematical Monthly, Vol. 29, No. 7 (August 1922), pp. 252–253
The post Queens on a prime order board first appeared on John D. Cook.2026-06-21 05:41:16
I’ve written a couple posts lately on getting an LLM to generate code to solve chess problems. The first used Claude to generate Prolog and the second used ChatGPT to generate Prolog. This post will use Claude to generate Z3/Python code.
The puzzle is one I’ve written about before:
Place all the pieces—king, queen, two bishops, two knights, and two rooks—on a 6 × 5 chessboard, with the requirement that the two bishops be on opposite colored squares and no piece is attacking another.
Incidentally, it’s common for “piece” to exclude pawns, as above. But then what do you call all the things on a chessboard? You might call them “chess pieces,” in which case a pawn is a “chess piece” but not a “piece.” One convention is to use “chessmen” or simply “men” to include pieces and pawns.
This was the prompt I used.
Write Z3/Python code to find all solutions to the following chess puzzle.
Place all the pieces—king, queen, two bishops, two knights, and two rooks—on a 6 × 5 chessboard, with the requirement that the two bishops be on opposite colored squares and no piece is attacking another.
The code found 192 = 8 × 24 solutions. The factor of 8 comes from 23 ways of swapping the pairs of bishops, knights, and rooks. The script reports
Total raw solutions: 192 Unique solutions (deduplicating piece-pair swaps): 24 ── Solution 1 ── 0 1 2 3 4 0 . K . . N 1 . . . . B 2 . . R . . 3 Q . . . . 4 . . . R . 5 . B . . N King: (0,1) Queen: (3,0) Bishop1: (5,1) [light] Bishop2: (1,4) [dark] Knight1: (5,4) Knight2: (0,4) Rook1: (4,3) Rook2: (2,2) ── Solution 2 ── 0 1 2 3 4 0 N . . K . 1 B . . . . 2 . . R . . 3 . . . . Q 4 . R . . . 5 N . . B . King: (0,3) Queen: (3,4) Bishop1: (5,3) [light] Bishop2: (1,0) [dark] Knight1: (5,0) Knight2: (0,0) Rook1: (4,1) Rook2: (2,2) ... ── Solution 24 ── 0 1 2 3 4 0 B . . B . 1 N . . . . 2 . . . . Q 3 . . R . . 4 . R . . . 5 N . . K . King: (5,3) Queen: (2,4) Bishop1: (0,0) [light] Bishop2: (0,3) [dark] Knight1: (5,0) Knight2: (1,0) Rook1: (3,2) Rook2: (4,1)
Here’s the code.
"""
Chess Puzzle Solver using Z3
Place king, queen, 2 bishops, 2 knights, 2 rooks on a 6×5 board
such that:
- The two bishops are on opposite-colored squares
- No piece attacks any other piece
"""
from z3 import (
Int, Solver, Or, And, Not, Distinct, If,
sat, ForAll, Implies
)
import itertools
ROWS = 6
COLS = 5
TOTAL_CELLS = ROWS * COLS # 30
PIECES = ["king", "queen", "bishop1", "bishop2", "knight1", "knight2", "rook1", "rook2"]
N = len(PIECES) # 8 pieces
def cell(r, c):
return r * COLS + c
def pos_to_rc(pos):
return pos // COLS, pos % COLS
def color(r, c):
"""Square color: 0=light, 1=dark"""
return (r + c) % 2
def attacks_king(r1, c1, r2, c2):
return max(abs(r1 - r2), abs(c1 - c2)) == 1
def attacks_queen(r1, c1, r2, c2):
return (r1 == r2 or c1 == c2 or
abs(r1 - r2) == abs(c1 - c2))
def attacks_bishop(r1, c1, r2, c2):
return abs(r1 - r2) == abs(c1 - c2)
def attacks_rook(r1, c1, r2, c2):
return r1 == r2 or c1 == c2
def attacks_knight(r1, c1, r2, c2):
dr, dc = abs(r1 - r2), abs(c1 - c2)
return (dr == 1 and dc == 2) or (dr == 2 and dc == 1)
# Map piece index to its attack function
ATTACK_FN = {
0: attacks_king,
1: attacks_queen,
2: attacks_bishop,
3: attacks_bishop,
4: attacks_knight,
5: attacks_knight,
6: attacks_rook,
7: attacks_rook,
}
def solve_all():
solutions = []
# Each piece gets an integer position in [0, TOTAL_CELLS)
pos = [Int(f"pos_{p}") for p in PIECES]
s = Solver()
# All positions in valid range
for p in pos:
s.add(p >= 0, p
Related post: Lessons Learned With the Z3 SAT/SMT Solver
The post All pieces on a 6 by 5 board first appeared on John D. Cook.
2026-06-17 22:23:51
I’ve been testing Claude’s ability to generate Lean 4 code to prove theorems. I’ve written about a couple experiments that verified calculations. I did not write about my failed attempt to get Claude to formalize a proof of the pqr theorem for seminorms.
This time I asked Claude to formally prove the theorem from the previous post on partial fraction decomposition in an abstract setting. Unlike the previous experiments, I did not give it a proof or calculation to verify; I asked it to generate a proof.
This was the prompt:
Write a proof in Lean 4 for the following generalization of partial fraction decomposition.
If a ring R is a principle ideal domain (PID), then every element c of the field of fractions over R can be written in the form \[c = \sum_i \frac{a_i}{p_i^{r_i}}\]
where the p_i are nonassociate irreducible elements of R, the r_i are non-negative integers, and the elements a_i and p_i are relatively prime.
This was Claude’s immediate response:
I’ll work through this carefully, as it’s a substantial formalization task. Let me think through what’s available in Mathlib and what needs to be constructed.
This is a genuinely hard Lean 4 formalization problem. Let me think carefully about what’s in Mathlib, what the statement precisely means, and what proof strategy is realistic.
It also stated its overall proof strategy:
Proof strategy: Write
c = a/bin lowest terms. Factorb = ∏ pᵢ^rᵢ. Use the Chinese Remainder Theorem / Bezout identity to decomposea/binto partial fractions.
If I needed to prove the theorem by hand, this suggestion alone could be very helpful.
The first attempt generated code that would not build. As before, a lot of the problems seem to stem from things moving around in Mathlib due to refactorings. There are also occasional hallucinations.
I did not offer any help other than pasting in error messages after each failure. When working on a real problem, I’d be more interactive. But as a test, I just passively pasted error messages and tried again. It took 11 iterations, but I finally got a proof. The proof had five sections marked “sorry,” which is essentially a TODO note indicating an unproven assumption.
I asked if it could explain or remove the sorries, and it said it could remove three of them. But the generated code did not build and I hit a session limit before I could debug the code. Here is the code with five sorry sections.
/-
PartialFractions.lean (v11 — final)
-/
import Mathlib
open UniqueFactorizationMonoid
variable {R : Type*} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R]
structure PFDSummand (R : Type*) [CommRing R] where
prime : R
exponent : ℕ
numer : R
noncomputable def PFDSummand.val [CommRing R] [IsDomain R] (s : PFDSummand R) :
FractionRing R :=
algebraMap R (FractionRing R) s.numer /
algebraMap R (FractionRing R) (s.prime ^ s.exponent)
structure IsPFD [CommRing R] [IsDomain R] [IsPrincipalIdealRing R]
(terms : List (PFDSummand R)) (c : FractionRing R) : Prop where
irred : ∀ s ∈ terms, Irreducible s.prime
nonAssoc : ∀ s ∈ terms, ∀ t ∈ terms, s ≠ t → ¬Associated s.prime t.prime
coprime : ∀ s ∈ terms, IsCoprime s.numer s.prime
sum_eq : (terms.map PFDSummand.val).sum = c
private lemma algMap_ne_zero {a : R} (h : a ≠ 0) :
(algebraMap R (FractionRing R)) a ≠ 0 :=
map_ne_zero_iff _ (IsFractionRing.injective R (FractionRing R)) |>.mpr h
private lemma exists_num_denom (c : FractionRing R) :
∃ a b : R, b ≠ 0 ∧
(algebraMap R (FractionRing R)) a / (algebraMap R (FractionRing R)) b = c := by
obtain ⟨a, b, hb, hab⟩ := IsFractionRing.div_surjective (A := R) c
exact ⟨a, b, nonZeroDivisors.ne_zero hb, hab⟩
-- ======================================================================
-- §6 Bézout splitting
-- ======================================================================
private lemma bezout_split (x y : R) (hcop : IsCoprime x y)
(hx : x ≠ 0) (hy : y ≠ 0) (e : R) :
∃ s t : R, s * x + t * y = 1 ∧
(algebraMap R (FractionRing R) e) /
((algebraMap R (FractionRing R) x) * (algebraMap R (FractionRing R) y)) =
(algebraMap R (FractionRing R) (e * t)) / (algebraMap R (FractionRing R) x) +
(algebraMap R (FractionRing R) (e * s)) / (algebraMap R (FractionRing R) y) := by
obtain ⟨s, t, hst⟩ := hcop
refine ⟨s, t, hst, ?_⟩
have hxF : (algebraMap R (FractionRing R)) x ≠ 0 := algMap_ne_zero hx
have hyF : (algebraMap R (FractionRing R)) y ≠ 0 := algMap_ne_zero hy
have hxyF : (algebraMap R (FractionRing R)) x *
(algebraMap R (FractionRing R)) y ≠ 0 := mul_ne_zero hxF hyF
have hst_F : (algebraMap R (FractionRing R)) s * (algebraMap R (FractionRing R)) x +
(algebraMap R (FractionRing R)) t * (algebraMap R (FractionRing R)) y = 1 := by
have h := congr_arg (algebraMap R (FractionRing R)) hst
simp only [map_add, map_mul, map_one] at h; exact h
-- Prove: ι e / (ι x * ι y) = ι(e*t)/ι x + ι(e*s)/ι y
-- Strategy: show RHS = LHS via eq_div_iff, simplify, linear_combination.
symm
rw [eq_div_iff hxyF, add_mul, div_mul_eq_mul_div, div_mul_eq_mul_div]
-- Goal: ι(e*t)*(ι x*ι y)/ι x + ι(e*s)*(ι x*ι y)/ι y = ι e
-- The mul_comm on the product inside:
rw [show (algebraMap R (FractionRing R)) x * (algebraMap R (FractionRing R)) y =
(algebraMap R (FractionRing R)) y * (algebraMap R (FractionRing R)) x from mul_comm _ _]
-- Now: ι(e*t)*(ι y*ι x)/ι x + ι(e*s)*(ι y*ι x)/ι y = ι e
-- Use field_simp to clear remaining denominators
field_simp [hxF, hyF]
-- Now a polynomial goal: close with linear_combination
simp only [map_mul]
linear_combination (algebraMap R (FractionRing R) e) * hst_F
-- ======================================================================
-- §7 Coprime numerator reduction
-- ======================================================================
private lemma coprime_numer_exists {p : R} (hp : Irreducible p) (a : R) (n : ℕ) :
∃ a' q : R, a = a' + q * p ^ n ∧ IsCoprime a' p := by
rcases Classical.em (p ∣ a) with _h | h
· exact ⟨0, 0, by sorry, by sorry⟩
· exact ⟨a, 0, by ring,
isCoprime_comm.mpr ((irreducible_iff_prime.mp hp).coprime_iff_not_dvd.mpr h)⟩
-- ======================================================================
-- §8 Main theorem
-- ======================================================================
private def emptyPFD (c : FractionRing R) (hc : c = 0) :
∃ terms : List (PFDSummand R), IsPFD terms c :=
⟨[], { irred := by simp, nonAssoc := by simp, coprime := by simp,
sum_eq := by simp [hc] }⟩
private lemma isPFD_of_denom : ∀ (d : R) (e : R),
∃ terms : List (PFDSummand R),
IsPFD terms ((algebraMap R (FractionRing R) e) /
(algebraMap R (FractionRing R) d)) := by
intro d
induction d using UniqueFactorizationMonoid.induction_on_coprime with
| h0 =>
intro e; simp only [map_zero, div_zero]
exact emptyPFD 0 rfl
| h1 =>
intro e
-- Unit denominator: sorry for now (§9C)
exact ⟨[], { irred := by simp, nonAssoc := by simp,
coprime := by simp, sum_eq := by simp; sorry }⟩
| hpr =>
rename_i prime_elem exp hp_prime
intro e
have hp_irred : Irreducible prime_elem := irreducible_iff_prime.mpr hp_prime
obtain ⟨e', _q, _he, he'_cop⟩ := coprime_numer_exists hp_irred e exp
exact ⟨[⟨prime_elem, exp, e'⟩], {
irred := fun s hs => by
simp only [List.mem_singleton] at hs; subst hs; exact hp_irred
nonAssoc := fun s hs t ht hne => by
simp only [List.mem_singleton] at hs ht; subst hs; subst ht; exact absurd rfl hne
coprime := fun s hs => by
simp only [List.mem_singleton] at hs; subst hs; exact he'_cop
sum_eq := by
simp only [List.map_singleton, List.sum_singleton, PFDSummand.val]; sorry }⟩
| hcp =>
rename_i x y hrel ih_x ih_y
intro e
-- Handle the case where x = 0 or y = 0 directly
rcases eq_or_ne x 0 with rfl | hx
· -- x = 0: denominator = 0*y = 0, so quotient = 0
simp only [zero_mul, map_zero, div_zero]
exact emptyPFD 0 rfl
rcases eq_or_ne y 0 with rfl | hy
· -- y = 0: denominator = x*0 = 0, so quotient = 0
simp only [mul_zero, map_zero, div_zero]
exact emptyPFD 0 rfl
-- Both nonzero: apply Bézout splitting
-- IsCoprime x y from IsRelPrime x y (using IsRelPrime.isCoprime)
have hcop : IsCoprime x y := hrel.isCoprime
obtain ⟨s, t, _hst, hsplit⟩ := bezout_split x y hcop hx hy e
obtain ⟨terms_x, hpfd_x⟩ := ih_x (e * t)
obtain ⟨terms_y, hpfd_y⟩ := ih_y (e * s)
exact ⟨terms_x ++ terms_y, {
irred := fun s' hs' => by
rw [List.mem_append] at hs'
exact hs'.elim (hpfd_x.irred s') (hpfd_y.irred s')
nonAssoc := fun s' hs' t' ht' hne => by
rw [List.mem_append] at hs' ht'
rcases hs' with hs' | hs' rcases ht' with ht' | ht'
· exact hpfd_x.nonAssoc s' hs' t' ht' hne
· intro; sorry
· intro; sorry
· exact hpfd_y.nonAssoc s' hs' t' ht' hne
coprime := fun s' hs' => by
rw [List.mem_append] at hs'
exact hs'.elim (hpfd_x.coprime s') (hpfd_y.coprime s')
sum_eq := by
rw [List.map_append, List.sum_append, hpfd_x.sum_eq, hpfd_y.sum_eq]
-- Goal: ι(e*t)/ι x + ι(e*s)/ι y = ι e / ι(x*y)
-- hsplit: ι e/(ι x*ι y) = ι(e*t)/ι x + ι(e*s)/ι y
-- So: ι(e*t)/ι x + ι(e*s)/ι y = ι e/(ι x*ι y) = ι e/ι(x*y)
rw [← hsplit, map_mul] }⟩
theorem pid_partial_fraction_decomposition (c : FractionRing R) :
∃ terms : List (PFDSummand R), IsPFD terms c := by
obtain ⟨a, b, _hb, hc⟩ := exists_num_denom c
rw [← hc]; exact isPFD_of_denom b a
section IntExample
example (c : FractionRing ℤ) :
∃ terms : List (PFDSummand ℤ), IsPFD terms c :=
pid_partial_fraction_decomposition c
end IntExample
The post Formalizing a ring theorem with Lean 4 and Claude first appeared on John D. Cook.
