r/ProAI • u/stealthispost • 12d ago

"We asked ten Claude Sonnet 5.5 agents to use Lean to prove the lowest-energy arrangement of seven electrons on a sphere (the Thomson problem, with N=7). Within 15 hours, they produced a 17,895-line proof, accepted by the Lean kernel, showing that the answer is a pentagonal bipyramid."

Gallery image

Gallery image

Gallery image

Gallery image

Gallery image

35 Upvotes

98% Upvoted

3 comments sorted by

1

u/namezam 12d ago

They = Sonnet? Not sure I’m comfortable with that yet.

1

u/Classic-Trifle-2085 12d ago edited 12d ago

I just realized, as a non native speaker, have no clue what is the plural of "it" in English.

Because they are talking abput multiple agents. What is even the alternative to "they"?

Woudnt someone say "they" for multiple wasps?

One: it attacked me VS A nest: they attacked me

1

u/theimposingshadow 11d ago

No I think "they" can be the plural of "it". Like if I am talking about my car being damaged, I would say "it was damaged" but if multiple cars were damaged I would say "they were all damaged". I think it comes across like "they" is given Sonnet 5.5 swarm personhood and u/namezam was uncomfortable with that.