some examples of things that may be like this, human generated list, varying confidence and specificity:
nvidia drivers (reduced in severity now)
drivers in general?
interfaces between software in general?
laws and regulations, sometimes
social group conformance expectations, sometimes
biology, especially immunology, especially drug design that has to bypass immune system
prompt design for ais?
robotic controller algorithms, especially for walking, especially for all-terrain walking
robot software drivers (see: drivers)
some things that seem not like this:
pure math (usually?)
okay at least definitely not arithmetic
fundamental physics? I mean there is the whole relativity vs quantum thing and that feels at all related but noncentral
writing software near the beginning?
playing most sports, as a human? tenuous
drawing with a pencil
using youtube, reddit, possibly any given widely deployed consumer software
the generator that feels live to me here is like, things where entropy* accumulates in interfaces or is generated in interfaces in the system somehow. many of them involve human-generated complexity, but that seems optional; seems like you can get this in pure math between conflicting formal systems, where you need a theorem connecting things even though pre-theoretic intuitively they’re “obviously” the same thing (of course that “obvious” is sometimes wrong).
* except maybe not literally entropy, but rather like, boundedly-rational unpredictability. I guess by some definitions that’s entropy—the definition would involve microstates not predicted by a macro model, and in this case the macro model would be the simple view of a system.
Actually, I have been diving into some specific topics lately, and simultaneously formalizing the theorems in Lean to help with understanding. The amount of omissions and handwaving going on in “proofs” in textbooks is insane. (To the point where I am not smart enough to figure out how to fill in some omissions.)
And I know that textbooks often only present a summary of a proof, and cite a more detailed source. But sometimes there is no citation at all, and even in cases where a citation exists, it might not contain the missing details.
seems like you can get this in pure math between conflicting formal systems
Hm… I don’t feel like this is what’s happening in most cases I encounter? Once I have a detailed pen-and-paper set-theoretic proof, it’s mostly straightforward to translate that to Lean’s type theory.
some examples of things that may be like this, human generated list, varying confidence and specificity:
nvidia drivers (reduced in severity now)
drivers in general?
interfaces between software in general?
laws and regulations, sometimes
social group conformance expectations, sometimes
biology, especially immunology, especially drug design that has to bypass immune system
prompt design for ais?
robotic controller algorithms, especially for walking, especially for all-terrain walking
robot software drivers (see: drivers)
some things that seem not like this:
pure math (usually?)
okay at least definitely not arithmetic
fundamental physics? I mean there is the whole relativity vs quantum thing and that feels at all related but noncentral
writing software near the beginning?
playing most sports, as a human? tenuous
drawing with a pencil
using youtube, reddit, possibly any given widely deployed consumer software
the generator that feels live to me here is like, things where entropy* accumulates in interfaces or is generated in interfaces in the system somehow. many of them involve human-generated complexity, but that seems optional; seems like you can get this in pure math between conflicting formal systems, where you need a theorem connecting things even though pre-theoretic intuitively they’re “obviously” the same thing (of course that “obvious” is sometimes wrong).
* except maybe not literally entropy, but rather like, boundedly-rational unpredictability. I guess by some definitions that’s entropy—the definition would involve microstates not predicted by a macro model, and in this case the macro model would be the simple view of a system.
Actually, I have been diving into some specific topics lately, and simultaneously formalizing the theorems in Lean to help with understanding. The amount of omissions and handwaving going on in “proofs” in textbooks is insane. (To the point where I am not smart enough to figure out how to fill in some omissions.)
And I know that textbooks often only present a summary of a proof, and cite a more detailed source. But sometimes there is no citation at all, and even in cases where a citation exists, it might not contain the missing details.
Hm… I don’t feel like this is what’s happening in most cases I encounter? Once I have a detailed pen-and-paper set-theoretic proof, it’s mostly straightforward to translate that to Lean’s type theory.