From Newsgroup: comp.lang.prolog


Recently, the application of AI tools to
Erdos problems passed a milestone: an Erdos
problem (#728 https://www.erdosproblems.com/728)
was solved more or less autonomously by AI (after
some feedback from an initial attempt), in the
spirit of the problem (as reconstructed by the
Erdos problem website community), with the result
(to the best of our knowledge) not replicated in
existing literature (although similar results proven
by similar methods were located).

This is a demonstration of the genuine increase in
capability of these tools in recent months, and is
largely consistent with other recent demonstrations
of AI using existing methods to resolve Erdos problems,
although in most previous cases a solution to these
problems was later located in the literature, as
discussed in https://mathstodon.xyz/deck/@tao/115788262274999408 .
This particular case was unusual in that the problem
as stated by Erdos was misformulated, with a
reconstruction of the problem in the intended spirit
only obtained in the last few months, which helps
explain the lack of prior literature on the problem.
However, I would like to talk here about another
aspect of the story which I find more interesting
than the solution itself, which is the emerging AI-powered
capability to rapidly write and rewrite
expositions of the solution.

https://mathstodon.xyz/@tao/115855840223258103

Mild Shock schrieb:

Hats off to Claude!

Jeff Barnett schrieb:

Use Google and search on  "Claude's Cycles". The first hit is a PDF

on the Stanford.edu web site. If you copy the URL buried under that hit,
you will download the PDF or just click on the Google result.

https://www.google.com/url?sa=t&source=web&rct=j&opi=89978449&url=https://www-cs-faculty.stanford.edu/~knuth/papers/claude-cycles.pdf&ved=2ahUKEwjI7cfFxYWTAxWUHUQIHXnrABsQFnoECCMQAQ&usg=AOvVaw2ieck2cXsmBf_KGis1B3i2

Paper is 5 pages in length. A fried sent it to me. You only need to

pay attention to the above goobly gop if you don't trust my friends.

https://www-cs-faculty.stanford.edu/~knuth/papers/claude-cycles.pdf

--- Synchronet 3.21d-Linux NewsLink 1.2

From Newsgroup: comp.lang.prolog

Hi,

Resolution of Erd˝os Problem #728
We provide a writeup of a resolution of Erd˝os
Problem #728; this is the first Erd˝os problem
(a problem proposed by Paul Erd˝os which has
been collected in the Erd˝os Problems website [3])
regarded as fully resolved autonomously by an AI
system. The system in question is a combination of
GPT-5.2 Pro by OpenAI and Aristotle by Harmonic,
operated by Kevin Barreto. The final result of the
system is a formal proof written in Lean, which we
translate to informal mathematics in the present
writeup for wider accessibility.

a writeup of Aristotle’s Lean proof
https://arxiv.org/pdf/2601.07421

Aristotle: The Era of Vibe Proving is Here
https://aristotle.harmonic.fun/

Bye

Mild Shock schrieb:

Recently, the application of AI tools to
Erdos problems passed a milestone: an Erdos
problem (#728 https://www.erdosproblems.com/728)
was solved more or less autonomously by AI (after
some feedback from an initial attempt), in the
spirit of the problem (as reconstructed by the
Erdos problem website community), with the result
(to the best of our knowledge) not replicated in
existing literature (although similar results proven
by similar methods were located).

This is a demonstration of the genuine increase in
capability of these tools in recent months, and is
largely consistent with other recent demonstrations
of AI using existing methods to resolve Erdos problems,
although in most previous cases a solution to these
problems was later located in the literature, as
discussed in https://mathstodon.xyz/deck/@tao/115788262274999408 .
This particular case was unusual in that the problem
as stated by Erdos was misformulated, with a
 reconstruction of the problem in the intended spirit
only obtained in the last few months, which helps
explain the lack of prior literature on the problem.
However, I would like to talk here about another
aspect of the story which I find more interesting
than the solution itself, which is the emerging AI-powered
capability to rapidly write and rewrite
expositions of the solution.

https://mathstodon.xyz/@tao/115855840223258103

Mild Shock schrieb:

Hats off to Claude!

Jeff Barnett schrieb:

Use Google and search on  "Claude's Cycles". The first hit is a PDF

on the Stanford.edu web site. If you copy the URL buried under that
hit, you will download the PDF or just click on the Google result.

;

https://www.google.com/url?sa=t&source=web&rct=j&opi=89978449&url=https://www-cs-faculty.stanford.edu/~knuth/papers/claude-cycles.pdf&ved=2ahUKEwjI7cfFxYWTAxWUHUQIHXnrABsQFnoECCMQAQ&usg=AOvVaw2ieck2cXsmBf_KGis1B3i2

;
Paper is 5 pages in length. A fried sent it to me. You only need to

pay attention to the above goobly gop if you don't trust my friends.

;
https://www-cs-faculty.stanford.edu/~knuth/papers/claude-cycles.pdf
;

--- Synchronet 3.21d-Linux NewsLink 1.2

From Newsgroup: comp.lang.prolog


Hi,

Ross Finlayson schrieb:

Three decades in software engineering helps read code.

Thats not much. Given that I wrote
an Euler Number computation to 1000
digits in Z-80 Assembler when I was

< 13 years old, I have > 5 decades
of software engineering.

LoL

Bye

Ross Finlayson schrieb:

On 03/07/2026 07:21 AM, Ross Finlayson wrote:

On 03/07/2026 03:08 AM, Mild Shock wrote:

Hi,

Resolution of Erd˝os Problem #728
We provide a writeup of a resolution of Erd˝os
Problem #728; this is the first Erd˝os problem
(a problem proposed by Paul Erd˝os which has
been collected in the Erd˝os Problems website [3])
regarded as fully resolved autonomously by an AI
system. The system in question is a combination of
GPT-5.2 Pro by OpenAI and Aristotle by Harmonic,
operated by Kevin Barreto. The final result of the
system is a formal proof written in Lean, which we
translate to informal mathematics in the present
writeup for wider accessibility.

a writeup of Aristotle’s Lean proof
https://arxiv.org/pdf/2601.07421

Aristotle: The Era of Vibe Proving is Here
https://aristotle.harmonic.fun/

Bye

Mild Shock schrieb:

Recently, the application of AI tools to
Erdos problems passed a milestone: an Erdos
problem (#728 https://www.erdosproblems.com/728)
was solved more or less autonomously by AI (after
some feedback from an initial attempt), in the
spirit of the problem (as reconstructed by the
Erdos problem website community), with the result
(to the best of our knowledge) not replicated in
existing literature (although similar results proven
by similar methods were located).

This is a demonstration of the genuine increase in
capability of these tools in recent months, and is
largely consistent with other recent demonstrations
of AI using existing methods to resolve Erdos problems,
although in most previous cases a solution to these
problems was later located in the literature, as
discussed in https://mathstodon.xyz/deck/@tao/115788262274999408 .
This particular case was unusual in that the problem
as stated by Erdos was misformulated, with a
reconstruction of the problem in the intended spirit
only obtained in the last few months, which helps
explain the lack of prior literature on the problem.
However, I would like to talk here about another
aspect of the story which I find more interesting
than the solution itself, which is the emerging AI-powered
capability to rapidly write and rewrite
expositions of the solution.

https://mathstodon.xyz/@tao/115855840223258103

Mild Shock schrieb:

Hats off to Claude!

Jeff Barnett schrieb:

Use Google and search on "Claude's Cycles". The first hit is a

PDF on the Stanford.edu web site. If you copy the URL buried under
that hit, you will download the PDF or just click on the Google

result.

https://www.google.com/url?sa=t&source=web&rct=j&opi=89978449&url=https://www-cs-faculty.stanford.edu/~knuth/papers/claude-cycles.pdf&ved=2ahUKEwjI7cfFxYWTAxWUHUQIHXnrABsQFnoECCMQAQ&usg=AOvVaw2ieck2cXsmBf_KGis1B3i2

Paper is 5 pages in length. A fried sent it to me. You only need

to pay attention to the above goobly gop if you don't trust my

friends.

https://www-cs-faculty.stanford.edu/~knuth/papers/claude-cycles.pdf

I trust my friends to have opinions,
not make my beliefs.

I have canon and dogma and doctrine for beliefs.

And "Research in Foundations".

Three decades in software engineering helps read code.

--- Synchronet 3.21d-Linux NewsLink 1.2

From Newsgroup: comp.lang.prolog


Hi,

Even ChatGPT can recognize it:

040C AF XOR A
040D 11 0000 LD DE,0000h
0410 CD3300 CALL 0033h
0413 21 0000 LD HL,0000h
0416 36 00 LD (HL),00h
0418 E5 PUSH HL
0419 D1 POP DE
041A 13 INC DE
041B 01 0904 LD BC,0409h
041E ED B0 LDIR
0420 3E 02 LD A,02h
0422 32 0000 LD (0000h),A

It responds with:

This is assembly language / machine code for a Zilog Z80
CPU (or a very close Z80-compatible processor). 🧠

The clues are the hex opcodes and instructions like:

AF → XOR A
CD → CALL
21 → LD HL,nn
32 → LD (nn),A
ED B0 → LDIR
CB 1C → RR H
E5 / D1 → PUSH HL / POP DE

These are classic Z80 instruction encodings.

Bye

https://chatgpt.com/share/69ad3f1e-0c68-8013-8cc3-b3f43267f69e

Mild Shock schrieb:

Hi,

Ross Finlayson schrieb:

Three decades in software engineering helps read code.

Thats not much. Given that I wrote
an Euler Number computation to 1000
digits in Z-80 Assembler when I was

< 13 years old, I have > 5 decades
of software engineering.

LoL

Bye

--- Synchronet 3.21d-Linux NewsLink 1.2

From Newsgroup: comp.lang.prolog

Hi,

The amazing things is ChatGPT, and possibly
other LLMs don't think linearly. I literally
posted the code like this:

040C AF
040D 11 0000
0410 CD3300
0413 21 0000
0416 36 00
0418 E5
0419 D1
041A 13
041B 01 0904
041E ED B0
0420 3E 02
0422 32 0000

XOR A
LD DE,0000h
CALL 0033h
LD HL,0000h
LD (HL),00h
PUSH HL
POP DE
INC DE
LD BC,0409h
LDIR
LD A,02h
LD (0000h),A

Two consecutive columns. And it moved
the columns side by side all on its own.
I noticed that many times,

that modern transformer AI architectur
has quite amazing visual perception,
even for ASCII input.

Have to double check whether it already
used GPT 5.3, or only GPT 5.2:

Introducing GPT‑5.3‑Codex
Expanding Codex across the full spectrum
of professional work on a computer https://openai.com/index/introducing-gpt-5-3-codex/

Bye

Mild Shock schrieb:

Hi,

Even ChatGPT can recognize it:

040C AF        XOR A
040D 11 0000   LD DE,0000h
0410 CD3300    CALL 0033h
0413 21 0000   LD HL,0000h
0416 36 00     LD (HL),00h
0418 E5        PUSH HL
0419 D1        POP DE
041A 13        INC DE
041B 01 0904   LD BC,0409h
041E ED B0     LDIR
0420 3E 02     LD A,02h
0422 32 0000   LD (0000h),A

It responds with:

This is assembly language / machine code for a Zilog Z80
CPU (or a very close Z80-compatible processor). 🧠

The clues are the hex opcodes and instructions like:

AF → XOR A
CD → CALL
21 → LD HL,nn
32 → LD (nn),A
ED B0 → LDIR
CB 1C → RR H
E5 / D1 → PUSH HL / POP DE

These are classic Z80 instruction encodings.

Bye

https://chatgpt.com/share/69ad3f1e-0c68-8013-8cc3-b3f43267f69e

Mild Shock schrieb:

Hi,

Ross Finlayson schrieb:
  > Three decades in software engineering helps read code.

Thats not much. Given that I wrote
an Euler Number computation to 1000
digits in Z-80 Assembler when I was

< 13 years old, I have > 5 decades
of software engineering.

LoL

Bye

--- Synchronet 3.21d-Linux NewsLink 1.2

From Newsgroup: comp.lang.prolog

Hi,

Maybe some 2D Diagrammtical Reasoning concerning
ASCII Texts , is result of training the AI on
corpus of math texts that contains usually a

lot of 2D typography. One can test the following.
I was juggling with Smarandache Dual numbers, so
I asked ChatGPT and DeepSeek about the following epsilon:

(1 -1)
(1 -1)

------- ChatGPT Protocoll begin ----------------

Q: Isn't this a Smarandache Dual number epsilon:

(1 -1)
(1 -1)

A: /* It computes A^2 which gives 0 and concludes: */
So your matrix is a valid matrix model of the
dual unit, just not the canonical one.

------- ChatGPT Protocoll end ----------------

------- DeepSeek Protocoll begin ----------------

Q: Isn't this a Smarandache Dual number epsilon:

(1 -1)
(1 -1)

A: /* It computes M^2 which gives 0 and concludes: */
Could represent ϵ itself if one redefines the basis
for dual numbers in the algebra of 2×2 matrices
generated by M and I, but that would not match
standard textbooks’ notation.

------- DeepSeek Protocoll end ----------------

But ChatGPT and DeepSeek are not omnicient enough
to even find the source of A resp. M:

https://fs.unm.edu/DualNumbers.pdf

So they didn't do retrieval. They did some little
mathematical reasoning on their own.

Have Fun!

Bye

Mild Shock schrieb:

Hi,

The amazing things is ChatGPT, and possibly
other LLMs don't think linearly. I literally
posted the code like this:

040C AF
040D 11 0000
0410 CD3300
0413 21 0000
0416 36 00
0418 E5
0419 D1
041A 13
041B 01 0904
041E ED B0
0420 3E 02
0422 32 0000

XOR A
LD DE,0000h
CALL 0033h
LD HL,0000h
LD (HL),00h
PUSH HL
POP DE
INC DE
LD BC,0409h
LDIR
LD A,02h
LD (0000h),A

Two consecutive columns. And it moved
the columns side by side all on its own.
I noticed that many times,

that modern transformer AI architectur
has quite amazing visual perception,
even for ASCII input.

Have to double check whether it already
used GPT 5.3, or only GPT 5.2:

Introducing GPT‑5.3‑Codex
Expanding Codex across the full spectrum
of professional work on a computer https://openai.com/index/introducing-gpt-5-3-codex/

Bye

Mild Shock schrieb:

Hi,

Even ChatGPT can recognize it:

040C AF        XOR A
040D 11 0000   LD DE,0000h
0410 CD3300    CALL 0033h
0413 21 0000   LD HL,0000h
0416 36 00     LD (HL),00h
0418 E5        PUSH HL
0419 D1        POP DE
041A 13        INC DE
041B 01 0904   LD BC,0409h
041E ED B0     LDIR
0420 3E 02     LD A,02h
0422 32 0000   LD (0000h),A

It responds with:

This is assembly language / machine code for a Zilog Z80
CPU (or a very close Z80-compatible processor). 🧠

The clues are the hex opcodes and instructions like:

AF → XOR A
CD → CALL
21 → LD HL,nn
32 → LD (nn),A
ED B0 → LDIR
CB 1C → RR H
E5 / D1 → PUSH HL / POP DE

These are classic Z80 instruction encodings.

Bye

https://chatgpt.com/share/69ad3f1e-0c68-8013-8cc3-b3f43267f69e

Mild Shock schrieb:

Hi,
;
Ross Finlayson schrieb:
;  > Three decades in software engineering helps read code.
;
Thats not much. Given that I wrote
an Euler Number computation to 1000
digits in Z-80 Assembler when I was
;
< 13 years old, I have > 5 decades
of software engineering.
;
LoL
;
Bye

--- Synchronet 3.21d-Linux NewsLink 1.2