The real value is in mixed mode:

- Lean supports calling out as a tactic, allowing you to call LLMs or other AI as judges (ie, they return a judgment about a claim)

- Lean can combine these judgments from external systems according to formal theories (ie, normal proof mechanics)

- an LLM engaged in higher order reasoning can decompose its thinking into such logical steps of fuzzy blocks

- this can be done recursively, eg, having a step that replaces LLM judgments with further logical formulations of fuzzy judgments from the LLM

Something, something, sheaves.