Thread 16775742

>let's just forget about Brouwer and focus on the pragmatic side of mathematics, surely nothing wrong can come from that
>

>>16775742 (OP)
if Brouwer had seen his name associated with “[math]\infty[/math]-categories” he would have quit mathematics and started designing gas chambers

can you retards tell me why the idris compiler is so buggy, i installed it in a google colab shell and it can't even read files, tells me there's no module named system or system.io

>>16775995
Because close to one third of all issues on their Github are still open, some going back more than a decade? https://github.com/idris-lang/Idris-dev/issues?q=is%3Aissue%20state%3Aopen%20sort%3Acreated-asc
But besides, I don't know the solution but there might not be, you shouldn't expect a toy language to be able to run properly in an ultra-special sandboxed environment. Maybe it says there's no system module because it can't provide it to you when it is embedded in a web service running in browser.
Off-topic though.

>>16775742 (OP)
link for the talk?

>>16775742 (OP)
She owes me sex

>>16776085
https://www.youtube.com/watch?v=d0uRPaJDTVs

>>16776092
thanks

>>16775742 (OP)
>Pragmatic side of math
Given that it's POPL I'm assuming she's suggesting using FM for math. Which is completely sound. Terry Tao talks about it nonstop nowadays

>>16776224
Yeah, Lean in particular. This is Emiy Riehl though. She works on Category Theory and she wrote the most memed (albeit good) introductory book on it. Her final goal is to make HomoTopy Type Theory the foundation of mathematics so everyone can learn Category Theory.

Speaker opened by acknowledging Martin Luther King Jr. Day and read an excerpt from King’s 1964 Nobel Peace Prize speech emphasizing faith, perseverance, and the possibility of justice and equality.
The speaker is representing the mathematical community and described recent formalization successes: the Feit–Thompson/odd order theorem efforts, the Flyspeck (Kepler) project, Peter Scholze’s “liquid tensor” challenge, and a cubical-Agda formalization that computed an unexpected value (−2) for a homotopy-group invariant.
Their focus is on formalizing results in their field, infinite-dimensional (∞) category theory. Two active projects are preparing background formalization work: one in Lean (led by Mario Carneiro and Dominic) and one in the Rzk proof assistant (by Nikolai Kiselev and Jonathan Weinberger).
The speaker warns ∞-category literature is particularly hard to formalize: papers often omit precise definitions, contain sketches, gaps, or morally-correct but incomplete proofs. They invoke Terry Tao’s three-stage metaphor (informal rigorous intuitive+rigor) to explain how much of the field lives between stages and how Lurie’s foundational work deliberately avoids fixing a single formal model, instead explaining ideas for experts to fill in details.

Continued examples showing how ∞-category literature often omits full proofs or definitions: Lurie’s selective foundations; Freed referencing Lurie’s sketch proof of the cobordism hypothesis; Gaitsgory & Rozenblyum leaving several statements unproven; Kapranov–Voevodsky’s homotopy-hypothesis paper contradicted later by Simpson, with ambiguity about where the original proof erred.
Anecdote: errors in published work (including by a Fields Medalist) motivated some mathematicians to pursue computer formalization.
Key question raised: can proof assistants handle literature that is “post‑rigorous” (sketchy foundations, conjectures used as assumptions)? The speaker argues yes in many cases:

One can formalize by axiomatizing the necessary properties (proof‑modulo / black‑boxing constructions) and later provide models.
Proof assistants support admitting theorems without proofs (sorries) so teams can split work between scaffolding and filling details—raising sociological issues of credit.
Incorrect proofs should fail to formalize, helping detect errors.

The speaker will describe three strategies to formalize ∞‑category theory; the first is “analytic”: pick a concrete model (e.g., quasi‑categories), formalize definitions in set‑theoretic terms, and proceed combinatorially.

>>16776253
Was Lean HTT? I thought it was calculus of inductive constructions like rocq. Or is she working on a HTT one?

Anyway category theory people are all delusional.

Three strategies to formalize ∞‑category theory were contrasted:
Analytic: pick a concrete model (e.g., quasi‑categories) and formalize combinatorially.
Axiomatic (strategy 2): develop a model‑independent framework (e.g., an "∞‑cosmos") in traditional foundations and prove general theorems about it, later showing models satisfy the axioms.
Synthetic (strategy 3): build domain‑specific foundations/type theory (e.g., a simplicial extension of homotopy type theory) and implement it in a tailored proof assistant (not typically possible in Lean).
Clarified difference between strategies 2 and 3: both are “synthetic” vs analytic, but strategy 2 is expressed in standard foundations (ZFC/type theory) while strategy 3 uses an exotic foundation optimized for the subject (e.g., cubical/HoTT variants).
Q&A: semantics of bespoke foundations are understood on paper but not fully formalized yet.
Lean project described:
Launched fall, co‑led by Mario, Dominic, and the speaker; uses mathlib and established Lean workflows (blueprint, dependency graph, Zulip).
Lean encodes ordinary categories via types of objects, dependent hom types, identity, composition, and laws.
Quasi‑categories give an analytic model for ∞‑categories but are fiddly to formalize: infinite coherence and weakened composition make many constructions intricate.
Practical plan: reuse mathlib’s existing ordinary/2‑category/enriched category developments and formalize ∞‑category theory by abstracting it as an ∞‑cosmos (an enriched/2‑category of ∞‑categories) so many categorical notions (adjunctions, limits, Kan extensions) follow from existing two‑category theory.
Caveat: verifying non‑vacuity (showing models satisfy the ∞‑cosmos axioms) remains a hard task.

The Lean ∞‑cosmos work must ultimately be tied to an analytic model (e.g., quasi‑categories); showing non‑vacuity (models satisfy the ∞‑cosmos axioms) is hard but envisioned as a focused effort (bounties for key lemmas).
Project progress: since September they formalized enriched‑limit pieces and the definition of an ∞‑cosmos (supporting code is being PR'd). They adopted incremental shipping—formalize small lemmas early.
Practical pain points in Lean:

Confusion between “functor as big structure” vs. “functor as morphism in Cat” leads to many boilerplate transports and repeated annotations; proofs become cluttered with steps that should be implicit.
Dependent‑type bookkeeping for 2‑cells/pasting diagrams: equality of boundaries forces transports, making composability checks awkward. As a result some theorems were proved only for Cat (componentwise) rather than for arbitrary 2‑categories; some cases have since been resolved but many similar issues remain.

Syn

thetic approach (strategy 3, in Rzk):
Use a simplicial extension of homotopy type theory where types are primitive ∞‑groupoids; identity types encode higher paths so ∞‑structures become natural.
In that system one can give a direct definition of ∞‑categories (composition witnessed by unique composites, coherence encoded by identity types) and formalize it in a proof assistant built for the foundation.
The approach aims to make ∞‑category theory more teachable and direct to formalize; the foundational semantics are understood on paper and parts of the system/definition have been formalized.

Rzk (Res/Rezk) project: implements a simplicial/HOTT-style foundation (not quasi‑categories) and already formalizes deeper ∞‑category theorems more easily than the Lean analytic approach; goal includes formalizing the Yoneda lemma and adjunctions.
Tradeoffs:
Synthetic foundations (Rzk) make many constructions concise and feel like ordinary 1‑category theory; proofs become short and conceptual.
But synthetic formalisms are currently isolated from large libraries (mathlib); porting results between foundations is nontrivial.
Practical concerns raised in audience Q&A:
Peer review of mechanized proofs: artifact review often happens post‑acceptance in PL community; for math, formalization could improve rigor and speed review but raises questions about who verifies foundations and definitions.
Analogy to programming languages: analytic = low‑level (quasi‑categories), axiomatic/∞‑cosmos = embedded DSL in Lean, synthetic = new language/foundation (Rzk/cubical systems). This frames many problems as CS challenges requiring collaboration.
Interoperability: proofs in HoTT can be expressed in Rzk when models overlap, but importing proofs between different proof assistants/foundations is difficult; Rzk could not import existing HoTT proofs and had to rework background development.
Social/technical point: formalization will require stronger collaboration between mathematicians and computer scientists; tooling, APIs, and tactics will determine usability and adoption.

>>16776259
>Was Lean HTT? I thought it was calculus of inductive constructions like rocq. Or is she working on a HTT one?
Well, she's not taking anything over currently, I don't think. It just seems they're using Lean.

>Anyway category theory people are all delusional.
I mean, it's basically just Petri Nets on crack, LSD and steroids.

>>16776271
Leans alright. Co(I)C is based. Isabelle and HOL are for losers.

>Petri nets
C'mon I piss on cat theorists as much as the next guy but they're nothing alike.

>>16775742 (OP)
The entire category drama fits into ZF + global choice function + Grothendieck-Tarski axiom assertting that for every x, there is a set u containing x and stable by pairs, subset of parties and indexed union (which is equivalent to say that every cardinal is smaller than an inaccessible cardinal). This is literally stated in SGA4 where Topoi are defined (the book is basically self-contained and doesn't require the heavy machinery of schema and other EGA topics to be read).

HoTT and all the typing delirium aren't necessary at all and aren't the minimalistic kernel people claim it is (you need inacessible cardinals in order to prove these systems are consistent anyways).

>>16776296
Isn't this argument analogous to saying it's "not necessairy" to use Linux because you can crack Windows or whatever?

>>16776273
>they're nothing alike.
https://yewtu.be/watch?v=WLkMBMUk48E&t=2921
Literally the first example she mentions about the application of category theory.

>>16776393
>>16776273
Oh sorry, here's the direct Youtube link.
https://www.youtube.com/watch?v=WLkMBMUk48E&t=2921

>>16776259
No, only Lean2 have support for HoTT, but it's deprecated. Lean4 uses dependent type. You need Agda if you want to play around with HoTT stuff.

>>16776310
no, its saying you don't need windows(pure category theory) because linux(set theory) has wine