The article isn’t about automatic proofs, but it’d be interesting to see a LLM that can write formal proofs in Coq/Lean/whatever and call external computer algebra systems like SageMath or Mathematica.

it cuts out the middle man of having to find facts on your own

Nope.

Even without corporate tuning or filtering.

A language model is useful when you know what to expect from it, but it’s just another kind of secondary information source, not an oracle. In some sense it draws random narratives from the noosphere.

And if you give it search results as part of input in hope of increasing its reliability, how will you know they haven’t been manipulated by SEO? Search engines are slowly failing these days. A language model won’t recognise new kinds of bullshit as readily as you.

Education is still important.

Sure, they’re just typically from the same industry with similar perspectives, similar blind spots and similar affinity for rants on topics X, Y and Z. Some get annoyed by this after a while so ignoring comments is a valid choice if you feel like that.

Probably. Still, it might be useful for blog discovery. One doesn’t have to read the comments.

Many such articles are reposted on HackerNews occasionally: https://news.ycombinator.com/