9 ms·

I wonder why we have yet to see more systematic exploration of Math. Anthropic describes that Claude identified a set of possibilities and then explored them u

by sosodev 1mo ago

I wonder why we have yet to see more systematic exploration of Math. Anthropic describes that Claude identified a set of possibilities and then explored them using sub-agents. The human saying "I believe in you" could literally just be something along lines of a harness with a /goal loop. We all identify this as absurd because... it's so lacking in rigor despite making major progress. What if we just applied a little more rigor? Ask the model to identify many possibilities, encode them, fan it out to other agents, loop them all, collect the results, etc. Then what happens? It feels like we have weak AGI and a decent system for discovery could transform it into weak ASI. That in turn could yield strong AGI and so on. I suppose that's what the Discovery Loop announcement was all about.

johnnienaked 1mo ago
I wouldn't be surprised if half these proofs turn out to be well crafted hallucinations, barring of course the ones actually verified in Lean
- evenhash 1mo ago
  Being “verified in Lean” doesn’t magically solve the problem of hallucinations unfortunately. It just shifts the work from > reading the (natural language) proof and confirming it has no errors to > reading the Lean code and confirming it correctly encodes the theorem For example here is a statement of the Pythagorean theorem in Lean: theorem EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ p₃ : P) : dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ <-> angle p₁ p₂ p₃ = Real.pi / 2 This is just one possible way of formalizing it and it depends on other definitions, wherein you also need to understand the assumptions they make, etc. Answering the question of “whether proving this theorem in Lean proves the Pythagorean theorem” thus requires expert judgement as well as domain knowledge of Lean’s libraries. So if the AI says “this theorem is true, here is the proof in Lean” it’s still possible that it’s not correct, even if the Lean code compiles. The result will still be in question until a human expert reviews it.
gessha 1mo ago
> I wonder why we have yet to see more systematic exploration of Math. > 60 Claude subagents
- sosodev 1mo ago
  I don’t find that to be particularly systematic because it’s still so haphazard. It’s like asking Claude to vibe code you a website.
  - gessha 1mo ago
    I was mostly highlighting the sheer cost of systematically exploring it. 60 agents doing something very narrow with a domain expert navigating the slop is already a high cost but I can see it being done more often in the near future since it just wasn’t possible a few years ago.
    - sosodev 1mo ago
      Ah, yeah that's a fair point. I was thinking it'd be something the labs themselves, or other companies with billions of dollars in funding, would tackle. The labs seemingly have the most to gain since such a system could be used for recursive self improvement.

by sosodev 1mo ago

johnnienaked 1mo ago

I wouldn't be surprised if half these proofs turn out to be well crafted hallucinations, barring of course the ones actually verified in Lean

evenhash 1mo ago
Being “verified in Lean” doesn’t magically solve the problem of hallucinations unfortunately. It just shifts the work from > reading the (natural language) proof and confirming it has no errors to > reading the Lean code and confirming it correctly encodes the theorem For example here is a statement of the Pythagorean theorem in Lean: theorem EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ p₃ : P) : dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ <-> angle p₁ p₂ p₃ = Real.pi / 2 This is just one possible way of formalizing it and it depends on other definitions, wherein you also need to understand the assumptions they make, etc. Answering the question of “whether proving this theorem in Lean proves the Pythagorean theorem” thus requires expert judgement as well as domain knowledge of Lean’s libraries. So if the AI says “this theorem is true, here is the proof in Lean” it’s still possible that it’s not correct, even if the Lean code compiles. The result will still be in question until a human expert reviews it.

gessha 1mo ago

> I wonder why we have yet to see more systematic exploration of Math. > 60 Claude subagents

sosodev 1mo ago
I don’t find that to be particularly systematic because it’s still so haphazard. It’s like asking Claude to vibe code you a website.
- gessha 1mo ago
  I was mostly highlighting the sheer cost of systematically exploring it. 60 agents doing something very narrow with a domain expert navigating the slop is already a high cost but I can see it being done more often in the near future since it just wasn’t possible a few years ago.
  - sosodev 1mo ago
    Ah, yeah that's a fair point. I was thinking it'd be something the labs themselves, or other companies with billions of dollars in funding, would tackle. The labs seemingly have the most to gain since such a system could be used for recursive self improvement.