There is a post[1] on the gitbutler blog where they collect a subset of defaults that allegedly git core developers use. It's where I got most of my config from.
Is there any way to recover a "bricked" Clara color? I bricked mine while trying to install nickel and koreader. Haven't been able to recover it since.
I think you'll need to replace the mainboard with one from ifixit.
Not aware of a debug interface, but in the absence of that, you'll need to desolder the nand module and replace the files there with the help of another owner. The mobile read forums are where you can connect with fellow owners.
There is a market for that, indeed. Hardened container images and hardened CI actions have been a thing for a while, with some companies providing exactly that.
In my experience, lean will show that it's correct, but does it not lose the mathematical intuition that led to the result? As far as my experience goes, that's really hard to encode in lean itself.
Could we maybe get more information about the problem from the LLM trace itself here?
As proofs become more and more complex, we will need two AI pipelines: one to generate the LEAN proof, and a second one to extract useful lessons for mathematicians from the LEAN proof.
No, something truly better does not exist yet, but that doesn't mean that it won't. Lean is young compared to Isabelle or Rocq, but actually quite old in absolut terms (and especially in AI terms).
[1] https://blog.gitbutler.com/how-git-core-devs-configure-git