Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > sci.physics.relativity > #669516

Aristotle: The Era of Vibe Proving is Here (Re: Terrence Tao: On Jan 4, ChatGPT was able to produce a proof Erdos #728)

Cross-posted to 2 groups.

Show all headers | View raw

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
>>  >
>>
> 

Back to sci.physics.relativity | Previous | Next — Previous in thread | Next in thread | Find similar

Thread

Terrence Tao: On Jan 4, ChatGPT was able to produce a proof Erdos #728 (Re: AI solves probl;em Knuth was/is working on!) Mild Shock <janburse@fastmail.fm> - 2026-03-07 11:58 +0100
  Aristotle: The Era of Vibe Proving is Here (Re: Terrence Tao: On Jan 4, ChatGPT was able to produce a proof Erdos #728) Mild Shock <janburse@fastmail.fm> - 2026-03-07 12:08 +0100
    Re: Aristotle: The Era of Vibe Proving is Here (Re: Terrence Tao: On Jan 4, ChatGPT was able to produce a proof Erdos #728) Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-03-07 07:21 -0800
      Re: Aristotle: The Era of Vibe Proving is Here (Re: Terrence Tao: On Jan 4, ChatGPT was able to produce a proof Erdos #728) Ross Finlayson <ross.a.finlayson@gmail.com> - 2026-03-07 07:36 -0800
        Only, three decades in software engineering? Re: Aristotle: The Era of Vibe Proving is Here (Re: Terrence Tao: On Jan 4, ChatGPT was able to produce a proof Erdos #728) Mild Shock <janburse@fastmail.fm> - 2026-03-08 10:00 +0100
          Re: Only, three decades in software engineering? Re: Aristotle: The Era of Vibe Proving is Here (Re: Terrence Tao: On Jan 4, ChatGPT was able to produce a proof Erdos #728) Mild Shock <janburse@fastmail.fm> - 2026-03-08 10:19 +0100
            Amazing Visual Perception, even for ASCII Input [GPT 5.3] (Was: Only, three decades in software engineering?) Mild Shock <janburse@fastmail.fm> - 2026-03-08 10:34 +0100
              Visual Perception helps reading Matrices, Fractions, etc.. (Re: Amazing Visual Perception, even for ASCII Input [GPT 5.3]) Mild Shock <janburse@fastmail.fm> - 2026-03-08 20:21 +0100
    Re: Aristotle: The Era of Vibe Proving is Here (Re: Terrence Tao: On Jan 4, ChatGPT was able to produce a proof Erdos #728) x <x@x.net> - 2026-03-08 19:10 -0700
      Biobrain cannot digest "Artificial" in AI (Was: Aristotle: The Era of Vibe Proving is Here) Mild Shock <janburse@fastmail.fm> - 2026-03-09 11:21 +0100
        Prolog vendors don't understand Tabling anymore (Re: When Supercomputing discovered BFS) Mild Shock <janburse@fastmail.fm> - 2026-04-04 14:10 +0200
          Buddos Waterloo: Checkpoint McCune (Re: Prolog vendors don't understand Tabling anymore (Re: When Supercomputing discovered BFS) Mild Shock <janburse@fastmail.fm> - 2026-05-10 16:20 +0200
            Could ISAMORE anti-unification help? (Re: Buddos Waterloo: Checkpoint McCune) Mild Shock <janburse@fastmail.fm> - 2026-05-10 16:48 +0200

csiph-web