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

Groups > sci.physics > #895364

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)

Cross-posted to 2 groups.

Show all headers | View raw

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

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

Thread

Re: AI solves probl;em Knuth was/is working on! Mild Shock <janburse@fastmail.fm> - 2026-03-04 08:29 +0100
  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

csiph-web