AIs should be forced to show their work. Every tool they use, every program they generate and run in the background, and every logical inference. They should be forced to produce Lean or Rocq proofs or execution traces for all the computation they use. For facts, they should be able to produce sources. For any abstract reasoning, they should be able to break it down into explainable steps.
Then, on top of that, they should be able to explain any of that, at any level of detail, whether talking to an expert or a layperson.
That's an implementation preference, and you can have all of that today if you write your own harness. Vibe coding a cat meme generator doesn't need a Lean proof.
why?
Conversely, https://www.lesswrong.com/posts/fzeoYhKoYPR3tDYFT/beware-iso...