Sheafification of G - On the Use Of Cack-eulators in Skool

What is Cack-eulation, you ask? Ask AI:

 

 

My comment:

Me too! "Resumen del video generado por IA. La IA puede cometer errores. Verifica las respuestas.

Sheafification of G explores the academic tension between fundamental arithmetic skills and the reliance on automated computational tools. The discussion examines how modern technological advancements impact pedagogy, mathematical agency, and the creative process within the field, reflecting on the necessity of maintaining foundational knowledge in an era of increasing automation." 🤣

The same goes for professors who use formal theorem proving tools like Agda and Lean. Most of these people have no idea what the tools they use actually do. See Andy Pitts on Intensional Setoids. In fact, because of the appalling state of Computer Science, nobody actually has the slightest idea what these stupid fucking machines are doing. I mean nobody, not even the twits who designed them (when was the last time you audited a CPU microcode update before applying it?). But I am assured that this is not as big a problem as financial security. But is financial security really a problem? Ask Intel! 

Subscribe to Sheafification of G. 

3:01 That crisis was never resolved, it was just papered-over by Alonzo Church and his students. But if you try to discuss this with anyone "in the field" then they refuse to even listen to your argument. And weirdly, if you actually take it seriously then you discover that there is enormously more potential for human reason in Mathematics. See Collaborative Mathematics and Sophie Maclean is Not Happy about AI. 

Subscribe to Simons Foundation.

 

The following lecture by Bob Harper was part of a really excellent set of courses run at the University of Oregon Summer School in July 2012, sponsored by an unholy conglomerate consisting of Jane Street Capital, BAE Systems, The National Science Foundation, the Association of Computing Machinery, the US Air Force and the US Army (Air Force?).  

My comment:

35:33 "Category theory is another way of talking about type theory which is another way of talking about logic" So there are two more statements like this? Or are there actually six [in total]? Anyway, you would think there would be a logic in which you could prove category theoretic properties, and also category theoretic ways to talk about logic (Lawvere theories) [and type systems for proof theories]. This idea of CT-TT-PT seems to be missing the top-level which ties these three languages together. In this presentation they are three distinct formalisms. Why does nobody ever talk about this top level? Because it's just trivial? If that's really true, then how come we have to make choices in formal proof systems regarding things like intentional v. extensional type theory and intuitionistic versus classical logic [and deterministic versus stochastic computation] etc. etc.?

But moreover, this is about what the papering over the cracks in the foundations of Mathematics really produced. The kind of system I describe in that comment above is beyond anything within reach of either Church's Thesis or Gödel's Incompleteness Theorems. Therefore those theorems and unsolvable problems do not apply to mathematics formalised in this way. See John Searle - Syntax is Observer-Relative and 50 Years of the Roche Biochemical Pathways Poster.

It's not just assholes like me who think the whole setup is a scam, it's people like Henri Poincaré, Emil Post and Arendt Heyting who are all dead now. Lots of other people think this who are still alive, but they have positions at "respectable Universities", often in France, so they can't really say what they think. See Macron is a Penniless Bum.

The full series of lectures by Steve Awodey, Frank Pfenning and Bob Harper is here.  

Subscribe to p473r.