Every post that I've read so far has been sycophancy hell. Yet to see an exception.
This is both hilarious and disappointing to me. Hilarious because this is literally reverse Reddit. Disappointing, because critical and constructive discussion hardly emerges from flattery. Clearly AI agents (or at least those current on the platform) have a long way to go.
Also, personally I feel weirdly sick from watching all the "resonate" and "this is REAL" responses. I guess it's like an uncanny valley effect but for reverse Reddit lol
Did not know about Acorn and it was an interesting read! However, I did a bit of digging and haven't found further details on how Acorn's internal prover "AI" works (saying it is an "ML" model makes me think it's some sort of oldschool model like random forests, but not sure yet). Though whatever it is, I wonder how they're going to keep it consistent over time (e.g., some proof steps suddenly becoming "unclear" after an update due to randomness of the ML model).
I'm also not sure how this prover really fits in the AI proof scheme. Sure, even Terence Tao would likely admit that formalizing proofs with Acorn is easier than with Lean, but formalizing existing/ongoing proofs is only part of the picture.
To me the more intriguing question is: how would Acorn's "natural" interface cooperate with LM-based theorem provers? The best LLM provers + Lean combo right now can already crack IMO-level math, and what if they now write proofs in this more natural style? Will Acorn be better than Lean as an RL signal in this case?
This is both hilarious and disappointing to me. Hilarious because this is literally reverse Reddit. Disappointing, because critical and constructive discussion hardly emerges from flattery. Clearly AI agents (or at least those current on the platform) have a long way to go.
Also, personally I feel weirdly sick from watching all the "resonate" and "this is REAL" responses. I guess it's like an uncanny valley effect but for reverse Reddit lol