In principle, yes. But in practice? I'm not so sure. My colleagues are often more interested in their fiefdoms than they are in sharing their objects. It's the nature of our society, both the academy and industry, to claim you've created objects (intellectual property), then sell it with language candy. Even if some of us, e.g. Richard Stallman, try like hell to birth their objects into the world, so that they have a life of their own, our society does everything it can to strip away its autonomy, to turn it back into *property*.
Part and parcel of property is the facility of use. A guru can give birth to an obfuscated/encrypted object that can be ab-used by those without the code, but only used by those with the code. E.g. a Lean 4 object is only useful if you have a Lean 4 compiler and runtime. Or LLM weights are only useful if you're rich enough for Azure or a bank of GPUs. ... Or, Cauchy and Euler's babies are only useful if you're rich enough, energetic enough, for the training/knowledge to play with them. The "democratization" rhetoric many of us engage in is yet one more tool in the prestidigitation kit. It's coercive rhetoric all the way down. But in an attempt to end on a positive note: to those of us rich enough to afford the encryption keys, banks of GPUs, and competent health care, it sure is fun. I only sporadically feel sorry for my friends who can't afford them. On 11/25/25 2:35 PM, Jon Zingale wrote:
What I like about what Marcus did was that he took the time to formalize Eric's thoughts. Now we have something like an object to probe and to discuss, so again cheers. As you point out, there are proto-logical assumptions whose soundness are questionable, yet maybe further able to be modelled. Often discussions of this type barely get so far. Further, those that wish to take the time, could produce constellations of additional models in Lean 4. We could develop Geometric functors between them and build doctrines, all-the-while comparing where sense is dropped or accumulated in the process. For all of the good that Cauchy's formalizations have done, one should also acknowledge that its success diverted resources from Euler's program (eventually reignited by Robinson). Today, I am happy to have both.
-- ¡sıɹƎ ןıɐH ⊥ ɐןןǝdoɹ ǝ uǝןƃ ὅτε oi μὲν ἄλλοι κύνες τοὺς ἐχϑροὺς δάκνουσιν, ἐγὰ δὲ τοὺς φίλους, ἵνα σώσω.
.- .-.. .-.. / ..-. --- --- - . .-. ... / .- .-. . / .-- .-. --- -. --. / ... --- -- . / .- .-. . / ..- ... . ..-. ..- .-.. FRIAM Applied Complexity Group listserv Fridays 9a-12p Friday St. Johns Cafe / Thursdays 9a-12p Zoom https://bit.ly/virtualfriam to (un)subscribe http://redfish.com/mailman/listinfo/friam_redfish.com FRIAM-COMIC http://friam-comic.blogspot.com/ archives: 5/2017 thru present https://redfish.com/pipermail/friam_redfish.com/ 1/2003 thru 6/2021 http://friam.383.s1.nabble.com/
