[Ads-l] Word: golfing (reducing the length of a computer program or formal mathematical proof; not in OED)

[ADSGarson O'Toole]

Within an xtweet I encountered the word "golfing" in the domain of
artificial intelligence and formal mathematics.

[Explanation of "golfing" from Googe AI on April 16, 2026]
Golfing a proof (specifically in formal verification like Lean) is the
process of making a mathematical proof as short, concise, and
efficient as possible, often aiming for the minimum number of
characters or lines. It is similar to code golfing, where the goal is
to optimize the proof script to its most compact form while
maintaining correctness.
[End explanation]

Here is some background to help decode the xtweet which appears further below.

Recently, Frontier AI systems have been solving significant open
mathematical problems. Informal proofs generated by AI systems are
sometimes flawed because of hallucinations and faulty logic. Hence,
some mathematicians are now demanding rigorous formal proofs which are
verified. Currently, the most popular language used to express formal
mathematical proofs is called Lean.

Gauss is an autoformalization agent from Math Inc. for assisting human
expert mathematicians with the arduous task of formal verification.

Mathematician Paul Erdos was well known for proposing open
mathematical problems which are now referred to as "Erdos problems".

Xtwitter handle: Math, Inc. @mathematics_inc
Timestamp: 6:12 AM, Apr 16, 2026
https://x.com/mathematics_inc/status/2044717899944960037?s=20

[Begin excerpt]
In surprising news, GPT5.4 Pro just found a solution Erdos Problem #1196.
Now Gauss has formalized the proof of #1196!
The initial proof was 7.2K lines of Lean, done in ~5 hours. Subsequent
golfing has compressed it down to 4K lines. (sorry-free, with
comparator check)
[End excerpt]

Wikipedia has a pertinent article about "Code golf"
https://en.wikipedia.org/wiki/Code_golf

I found the term "golfing" in the xtweet context intriguing because it
was about Occam's razor and superhuman cognition.

Garson O'Toole

------------------------------------------------------------
The American Dialect Society - http://www.americandialect.org