John D. Cook

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, …, […] The post Queens on a prime order board first appeared on John D. Cook .

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 […] The post All pieces on a 6 by 5 board first appeared on John D. Cook .

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 […] The post Formalizing a ring theorem with Lean 4 and Claude first appeared on…

Nearly everyone who as seen partial fraction decomposition was introduced to it as a way to compute integrals. If P(x) and Q(x) are polynomials, then you can break their ratio P(x)/Q(x) into a sum of terms that can each be integrated in closed form. As with most topics in a calculus class, partial fractions go by in […] The post Partial fraction decomposition first appeared on John D. Cook .

You can’t prove a theorem by just checking a few examples. Except sometimes you can. A few weeks ago I wrote Pentagonal numbers are truncated triangular numbers. In a nutshell, if the pentagonal numbers are defined by Pn = (3n² − n)/2 and the triangular numbers by Tn = (n² + n)/2 then Pn = T2n − 1 − Tn − 1. Here’s a visualization […] The post Three examples suffice first appeared on John D. Cook .

The nth pentagonal number Pn is the number of dots in diagrams like those below with n concentric pentagons. We have the formula Pn = (3n² − n)/2 where n is a positive integer. If n is an integer but not positive, the equation above defines a generalized pentagonal number. If you’re given an n, you can easily compute Pn. […] The post Testing pentagonal numbers first appeared on John D. Cook .

I got an email message this afternoon reporting a typo in a blog post from about a year ago on converting between quaternions and rotation matrices [1]. The email said exactly where the typo was, but I decided to see whether Claude would find it. Specifically, I prompted Sonnet 4.6 Medium with the following. Write […] The post Quaternion Rotations, Claude, and Lean first appeared on John D. Cook .

A few days ago I wrote about using Claude to solve a chess puzzle by writing Prolog code. This morning I tried a similar chess puzzle with ChatGPT. The task is to place a queen, king, rook, bishop, and knight on a 4 by 4 chessboard so no piece attacks another. Of course there’s not […] The post Writing Prolog with ChatGPT first appeared on John D. Cook .

Back when the US government classified strong encryption as “munitions,” RSA public key cryptography was illegal to export. In 1995, Adam Back protested this by creating a terse, obfuscated implementation of RSA in Perl code and used it as an email signature. The code was also printed on T-shirts. The shirt was classified as munitions […] The post RSA munitions T-shirt first appeared on John D. C…

Prolog is the original logic programming language. The name comes from programming in logic. More specifically, the name comes from programmation en logique because the inventor of the language, Philippe Roussel, is French. Prolog has its advantages and disadvantages. One of the advantages is that the language represents logical problems directly. One of the disadvantages […] The post Solving a c…

I ran an experiment today to see whether Claude could generate Lean code to prove a calculation at the bottom of this post, six lines of calculus. I started with this prompt This page contains a mathematical proof that a Fourier coefficient, a_n, is given in terms of a Bessel function. The LaTeX source for […] The post Formally proving a calculation with Claude and Lean first appeared on John D. …

Often there’s a thread running through a sequence of my posts. Sometimes I make this explicit and sometimes I don’t. The latest thread started with this post commenting on a tweet that observed that exp(−x²) ≈ (1 + cos(sin(x + x))/2. Some people said online that that the approximation is simply due to the first […] The post Pulling on a thread first appeared on John D. Cook .

Kepler solved his eponymous equation M = E − e sin(E) by finding a fixed point of E = M + e sin(E). So guess a value of E and stick it into the right hand side. Then plug that value into the right hand side again. Kepler said a couple iterations should be enough. And a couple […] The post Aitken acceleration before Aitken first appeared on John D. Cook .

An earlier post discussed how to solve Kepler’s equation M = E − e sin(E) using a sine series. You could also solve Kepler’s equation using a power series, which Lagrange did in 1771. Both approaches express E as a function of e and M, but from different perspectives. Bessel thought of his solution as a sum of sines in […] The post The Laplace limit first appeared on John D. Cook .

I ran across a cranky formula for π based on physical constants here and decided to play around with it. The source describes λ as “wavelength (chosen in the microwave region)” and I thought perhaps you could chose a value of λ to make the equation work. But as a comment pointed out, the bracketed […] The post A crank formula for π first appeared on John D. Cook .

The previous post very briefly said that the integral representation for Bessel functions was motived by solving Kepler’s equation. This post will go into more detail. Kepler’s equation There are multiple ways to describe the position of a planet in an elliptical orbit around a star. For historical reasons, these descriptions have arcane names such […] The post From Kepler to Bessel first appeare…

Yesterday I wrote a post showing that the trapezoid rule evaluates the integral very efficiently. But how do we know what the exact integral is for comparison? If you ask Mathematica, it will tell you the integral equals −2π J1(1) where J1 is a Bessel function. This may seem like rabbit out of a hat, […] The post Mr. Bessel’s eponymous functions first appeared on John D. Cook .

One reason people study Latin is that it is the ancestor of many modern languages. English derives from West Germanic languages, not from Latin, but much of English vocabulary, perhaps as much as 60%, derives from Latin, either directly or indirectly through French. Knowing a bit of Latin makes sense of many things that would […] The post The Latin of Linux first appeared on John D. Cook .

Several posts lately have looked at the function f(x) = cos(sin(x) + x). This post will look at the function from a different angle. It’s a smooth function with period 2π, and it’s very flat at odd multiples of π, i.e. the first five derivatives are zero. For reasons I wrote about here, this means that […] The post Integrating smooth periodic functions first appeared on John D. Cook .

I was thinking more about the cosine approximation to the Gaussian exp(−z²) ≈ (1 + cos(sin(z) + z))/2 that I wrote about last week. The two expressions above are close along the real axis but not along the imaginary axis. If z = iy, the right side grows much faster than the left, behaving like exp(exp(y)). This led to […] The post Partitions over permutations first appeared on John D. Cook .