I agree. Lean5 maybe will be built around something like one of the type-theory-in-type-theories that are getting built with QIITs... concrete efficiency for these massive searchers seems important more than metaprogrammatic ergonomics. semirelated (for building upon hol-reflection) https://github.com/emberian/svenvs tries to do some explicitly self-verified self-improving confinement...
I've been sticking my head in the sand partly because it is so painful to watch these other communities slowly do the meaning-making that has already been done about these ... (read more)
I have some light intuitions into the way the realizability toposes ingress into the more localic models. "On-policy" can be fragile, arbitrarily fragile, for higher coherences. I have some studies (that I need to tidy up and publish...) about in-context learning of various logics and protocol families and the first error in a trajectory when corrected by human can lead to very long, complicated reasonings. Automated reasoning was a young field but double categories, parametricity, trace spaces, and metric enrichment all studied somewhat and (in my opinion... (read more)