🧵 What went wrong?
Anonymous at Sun, 16 Mar 2025 05:54:57 UTC No. 16620475
Anonymous at Sun, 16 Mar 2025 06:01:31 UTC No. 16620478
>>16620475
Paradox aversion, like every rigid ruleset.
Anonymous at Sun, 16 Mar 2025 20:16:50 UTC No. 16621110
>>16620478
ah yes, i forgot about paradox aversion
Anonymous at Sun, 16 Mar 2025 20:19:24 UTC No. 16621112
>>16620475
I've met one person who works in this field and it was the most deranged mentally ill trans person I've ever met, a walking stereotype
Anonymous at Sun, 16 Mar 2025 21:32:09 UTC No. 16621146
>>16621112
feel like this isnt the first time ive heard this one about this field
t. theoretical physicist on the outside looking in
Anonymous at Mon, 17 Mar 2025 05:17:11 UTC No. 16621382
>>16620475
their one hero died, the other hero got BTFO on a listserv mailing list and ragequit (not making this up)
Anonymous at Mon, 17 Mar 2025 07:13:17 UTC No. 16621426
>>16621382
who was the other hero?
Anonymous at Mon, 17 Mar 2025 07:22:23 UTC No. 16621433
>>16621426
https://fomarchive.ugent.be/fom/201
Anonymous at Mon, 17 Mar 2025 07:53:01 UTC No. 16621444
>>16620475
The H on the cover is missing its -.
Anonymous at Mon, 17 Mar 2025 17:17:47 UTC No. 16621742
>>16620475
From what I understand, the field was mostly dominated with young people who didn’t have a great understanding of mathematics outside of category theory and either very specialized algebraic topology (which relies in category theory to express some of its important theorems) or else Haskell programming. HoTT was originally intended just to formalize and automate proofs in algebraic topology. It’s designed for that and suited for that, but not a lot of these people were working on that basic question. Instead they were developing strange-looking highly technical theory in a field nobody else could understand, that may or may not be equivalent to existing work in other fields-it’s hard to know because nobody can understand it-and at the same time claiming this work will override and replace work in other fields that they in turn have not studied and do not understand. It was an emperors-clothes shitshow, the field is dead and buried, and it’s actually a pity because the system itself was fine and could still be used for its originally intended purpose, but now because of the stink nobody will take you seriously if you mention you like HoTT
Anonymous at Mon, 17 Mar 2025 18:38:51 UTC No. 16621775
>>16621433
>https://fomarchive.ugent.be/fom/20
looks very cordial to me
Anonymous at Mon, 17 Mar 2025 18:41:44 UTC No. 16621778
univalent foundations is a good replacement
Anonymous at Mon, 17 Mar 2025 21:24:25 UTC No. 16621929
>>16621778
how can i do univalent mathematics?
Anonymous at Tue, 18 Mar 2025 02:02:57 UTC No. 16622135
>>16621778
same thing
Anonymous at Tue, 18 Mar 2025 14:04:05 UTC No. 16622403
>>16621775
>spergs for a while about not getting enough respect
>refuses to answer questions explain his positions beyond “buy my book”
>cordially ragequits
My best guess is that he couldn’t engage with the questions in good faith without getting Cancelled by HoTT’s deranged fanbase, and he was smart enough to realize that
Faced with an impossible situation, it’s hard to blame him. Rather it’s a reminder to the rest of us to always proactively gatekeep
Anonymous at Tue, 18 Mar 2025 22:57:42 UTC No. 16623034
>>16620475
Our lord and savior, Vladimir Voevodsky died for our sins, and left us without guidance in the univalent magics on the earthly plane.
Anonymous at Wed, 19 Mar 2025 02:36:00 UTC No. 16623268
>>16620475
Yes, seems crazies got too involved. Happened with functional programming languages too.
Also, I suspect most mathematicians - as most academics - are not really interested in anything that upsets the priesthood.
Anonymous at Wed, 19 Mar 2025 10:01:25 UTC No. 16623460
It should be possible to explain the meaning of the equals sign to a first grader.
🗑️ Anonymous at Wed, 19 Mar 2025 13:20:19 UTC No. 16623591
>>16623034
>Volodomyr Vyivodskyy
Come on, it’s 2015
Anonymous at Wed, 19 Mar 2025 15:45:41 UTC No. 16623708
>>16620475
Probably because people became aware that ** classical logic ** based Curry-Howard correspondence is possible (with the need to allow backtracking realizers when excluded middle is used in the proof) and that the grand need to distort mathematics into strict so-called constructivism (in fact intuitionnist logic) in the name of computer science was misguided.
Besides, the management of the notion of equality in these systems is incomprehensible (unless you have a very strong background in algebraic topology and fibrations, making it unsuitable for foundations who should be understandable by beginners,at least for simple practical uses; I don't deny that the analogy between homotopy groupoids and collection of equality proofs is fascinating but this is for professionals). Compare with the simplicity of Leibniz equality.
Anonymous at Wed, 19 Mar 2025 16:45:26 UTC No. 16623731
>>16620475
abandonware
https://www.cl.cam.ac.uk/events/owl
https://xenaproject.wordpress.com/2
>What I have noticed amongst the univalent people is that, more than any of the other communities I’ve run into, they really do not seem to care about doing “fashionable mathematics”. I would love to be spammed with comments telling me that I was wrong about this. But my impression is that there are a whole bunch of interesting type theory questions raised by the univalence axiom, and that these foundational questions are what the community is on the whole interested in. I have asked lots of univalent people how it could possibly be the case that Voevodsky, someone who made their name by discovering a homotopy theory for schemes, could spend 15 years working in univalent type theory and still not have a definition of a scheme at the end of it. It has been explained to me, on more than one occasion, that Voevodsky’s interests changed. This is fine. But I still want the schemes. Here is a message for you univalent people — if you do not actually build some fashionable mathematics at some point, then we will not come in our masses. Where is the definition of a scheme? Where is the proof that the class group of a number field is finite? Where are number fields, for that matter? Can you really show me that it does not matter that all number fields are countably infinite, and hence biject with each other, and hence are equal, in your system? I know that’s not how it works and there’s more to it than that. But I don’t want to hear protestations, I want to see the code. UniMath, Arend, any system you like. I know you’re good at higher topos theory but where is the arithmetic? Where is quadratic reciprocity?
Anonymous at Wed, 19 Mar 2025 17:56:02 UTC No. 16623767
Type theory (and HoTT for that matter) is better than set theory and I say this as an algebraic topologist who likes pure set theory and wanted to study it for its own sake. Types are just inherently more intuitive for starters and don't come with the baggage of paradoxes set theory comes with.
Anonymous at Wed, 19 Mar 2025 21:58:46 UTC No. 16623925
>>16622403
>Dunning Krugers gatekeeping science
every time.
Anonymous at Thu, 20 Mar 2025 01:23:06 UTC No. 16624066
>>16623460
first graders care about [math]\mathbb N[/math]
>>16623731
>if you do not actually build some fashionable mathematics at some point, then we will not come in our masses. Where is the definition of a scheme? Where is the proof that the class group of a number field is finite?
kek this guy is just as bad, if he looks at scheme and thinks Fashionable
Anonymous at Thu, 20 Mar 2025 04:54:03 UTC No. 16624130
What's the simplest HoTT proof that 2+2=4 is a proposition?
Anonymous at Thu, 20 Mar 2025 05:40:34 UTC No. 16624140
>>16624066
>kek this guy is just as bad, if he looks at scheme and thinks Fashionable
dude spurred more momentum into formalised mathematics than any prior attempt. mathlib gets 150+ commits/week, a shit ton of grants and academic and industry mindshare. meanwhile the HoTT folks brag about how poor and esoteric they are. but ok bro, i'm sure you're publishing shit with greater influence than EGA
Anonymous at Thu, 20 Mar 2025 09:30:32 UTC No. 16624185
>>16620475
nobody wanted to be associated with homos
Anonymous at Thu, 20 Mar 2025 13:19:15 UTC No. 16624244
>>16621382
>their one hero
Vlad was early and had ambition and ideas of formalization of his algtop stuff, got in contact with the type theory crowd (Adwody etc.), who at a similar time discovered the importance of groupoids (the key thing in Vlad's complicated equality).
But he very quickly found the projects taken over by type theorists (who knew no algtop), and he disavowed the book project. Before he offed himself. For this reason, he at several points very strongly emphasized how his project is "Univalent Foundations" and how HoTT is the CS spinoff.
The tranny stuff is true, albeit the animosity towards trannies is over the top in right winged math grad circles. The tranny coders often are, indeed, smartasses. But that's just like any scala kids who learn about monads and the Yoneda lemma without knowing the first two terms of the exponential function (not hyperbole.)
But the haskell types to be smarter than your average coder also. Donno if that makes for good programs.
Anonymous at Thu, 20 Mar 2025 16:19:39 UTC No. 16624331
>>16624244
>Before he offed himself.
Is that what happened? Very sad if true.
>But the haskell types to be smarter than your average coder also. Donno if that makes for good programs.
Depends which “haskell type” you’re thinking of. The bad elements have all moved on to Rust afaict, which is ironic since Rust is not functional at all. Or maybe it’s a new generation of bad elements idk.
Anonymous at Fri, 21 Mar 2025 10:20:14 UTC No. 16624838
>>16624331
>Is that what happened?
Oh actually I might be midremembering. He has some problems, but I don't want to spread rumors either.
Anonymous at Fri, 21 Mar 2025 13:55:10 UTC No. 16624976
>>16621775
From my point of view, Harvey Friedman is evil!
Anonymous at Sat, 22 Mar 2025 02:42:02 UTC No. 16625539
>>16624244
Cute boy.
Anonymous at Sun, 23 Mar 2025 14:38:18 UTC No. 16626617
>>16623708
>Probably because people became aware that ** classical logic ** based Curry-Howard correspondence is possible (with the need to allow backtracking realizers when excluded middle is used in the proof)
i'd love to hear more about that
Anonymous at Mon, 24 Mar 2025 00:52:15 UTC No. 16627043
>>16626617
see e.g. https://www.irif.fr/~krivine/articl
https://www.irif.fr/~krivine/articl
There are also simple game semantics for first order logic where a classical (cut-free) proof can be turned into a winning strategy in a game derived from the formula where you'd lose if the game lasted forever (it is described in the second paper, I'd elaborate maybe later)
Anonymous at Mon, 24 Mar 2025 18:28:20 UTC No. 16627489
>>16627043
lovely stuff, thank you very much, have a great day
Anonymous at Mon, 24 Mar 2025 18:31:45 UTC No. 16627494
>>16627043
Oh, Whould you hapen to have anything on Paraconsisten logic?
Anonymous at Mon, 24 Mar 2025 22:58:19 UTC No. 16627703
>>16627494
No ...
Anonymous at Mon, 24 Mar 2025 23:09:08 UTC No. 16627712
>>16627494
>>16627703
The problem with these systems is that the implication has to be very ill behaved. Let us consider we are in a system of sentences in which 1°) for every sentences A,B, there is a third sentence "A -> B"
2°) whenever A and A-> B are "theorems" (whatever that means) in the system then B is also a theorem
3°) there is a special sentence "#" which reads literally "every sentence is true" and theoremhood behave accordingly (namely # -> X is a theorem in that system)
Note that intuitionistic logic is exactly like that (there is no really a negation in intuitionism, instead "not Y" is routinely defined as an abbreviation of Y -> #).
Of course when # is proven, every other sentence is. Which of the above wouldd you ban? 3° ?(paraconsistent logic was intended to allow more sentences in the name of solving paradoxes but why would be "every sentence is true" meaningless then?)
Anonymous at Tue, 25 Mar 2025 06:00:50 UTC No. 16628032
>>16627712
>but why would be "every sentence is true" meaningless then?
Mh, I don't think it is meanigles, But unless im missremembering, Paraconsistent logics allow for contradictory statements through the removal of the principle of explosion(& with it ad absurdum), with it ganing the ability to talk about contradictory statements without the theory being trivial, IE everithing being true, as for what i'd ban, çIm nor sure, dual-intuitionistic logic as a connective # known as pseudo-differnce whith which negation is attained so ¬A=(⊤#A), in much the same way that in paracomplete systems negation can be dffined as you said with a variation of implication that im going to denote @ & negation goes ¬A=(A@⊥), it's realy something
Anonymous at Tue, 25 Mar 2025 06:07:45 UTC No. 16628034
>>16621146
Man you people are easy to bully into groupthink
Let me try
Anon I heard marine biology is paying more now
Anonymous at Tue, 25 Mar 2025 06:30:06 UTC No. 16628036
>>16620475
Same thing that went wrong with Socrates, Copernicus and Galileo. Galileo was burned at the stake even in the face of a mountain of evidence, because he went against the Pope.
Anonymous at Tue, 25 Mar 2025 17:20:04 UTC No. 16628312
>>16628036
https://www.youtube.com/watch?v=SQA
Anonymous at Tue, 25 Mar 2025 20:46:40 UTC No. 16628461
>>16627043
PlatonicCHADS win again
Anonymous at Wed, 26 Mar 2025 17:03:22 UTC No. 16629113
>>16628312
exactly the kind of slop I always imagined euros.o.ys enjoying
Anonymous at Fri, 28 Mar 2025 14:30:55 UTC No. 16630891
>>16628312
Wtf is this garbage? lol
Anonymous at Fri, 28 Mar 2025 16:52:55 UTC No. 16631004
>>16629113
>euros
Brexit means Brexit, lard.
Anonymous at Sun, 30 Mar 2025 00:52:06 UTC No. 16632195
Why not map out the space of all supertheories that contains the likes of hott, nf, k-p sets to find a good surface?
Anonymous at Sun, 30 Mar 2025 07:34:19 UTC No. 16632311
>>16620475
Got taken over by do-nothing trannies, like the Rust programming language.
Anonymous at Mon, 31 Mar 2025 00:50:18 UTC No. 16633274
>>16631004
>all that work and effort
>still a fucking Eurotrash
This is what you look like to Americans, assuming your not a Paki or already murdered by a Paki
Anonymous at Tue, 1 Apr 2025 02:51:27 UTC No. 16634537
>>16632311
The parallels between rust in 2025 and hott in 2015 are actually quite remarkable. I donno how to explain it.
Anonymous at Wed, 2 Apr 2025 11:23:04 UTC No. 16634920
>>16634537
dogmatism and hubris what else
Anonymous at Wed, 2 Apr 2025 20:29:43 UTC No. 16635411
>>16620475
Is this what Jacob Lurie was cultivating? Please forgive me I've been out of the mathematical loop for almost a decade now
Anonymous at Thu, 3 Apr 2025 05:18:03 UTC No. 16635736
>>16620475
What's the point of a foundational theory that isn't set theory if the theory requires the use of sets?
Anonymous at Thu, 3 Apr 2025 05:43:36 UTC No. 16635752
>>16635736
Because set theory does have its place as a subset of combinatorics.
Anonymous at Thu, 3 Apr 2025 09:57:13 UTC No. 16635861
>>16635736
Sets are a defined notion in type theory.
Anonymous at Thu, 3 Apr 2025 10:07:14 UTC No. 16635870
>>16635736
foundations and so-called "top-down" thinking are mutually exclusive. The higher category machinery is meant to unify works in different areas, not to say what math is.
Anonymous at Thu, 3 Apr 2025 10:15:29 UTC No. 16635875
>>16621112
>>16621146
Troops are attracted to “alternatives to set theory” because set theory requires a lot of work to get to SOTA, where as alternative foundations aren’t nearly as developed so you can reach their frontiers more quickly. Of course you just wind up having to redevelop what set theory has already come up with. It’s kinda like trains obsessed with porting modern games to 80s consoles. They get the thrill of accomplishing something novel because no one would ever bother to do something that way.
Anonymous at Thu, 3 Apr 2025 13:08:05 UTC No. 16636026
>>16635875
Troons flock towards good things to be seen as good by proxy, to cover for the fact that their mere existence is an act of degeneracy.
Set theory, as conceived in material set theories such as ZFC, has never been anything but a clunky mess of mystifying garbage as a foundation of mathematics, and so it's only natural that it's the greatest contribution of jewish minds to the field of mathematics. Its "SOTA" is pure pipul over ultimately irrelevant issues that furthers not one bit our understanding of mathematics and logic as a whole. Type theory has direct, practical utility thanks to its connection to computation and computers, and it has actual philosophical ramifications that are worth studying, implicating all of mathematics.
Anonymous at Thu, 3 Apr 2025 17:35:33 UTC No. 16636228
>>16636026
Type theory is overbloated and abstruse while every concept can be translated straightforwardly into ZF + global choice operator T (a map such that for every predicate x -> P(x) we have forall t, P(t) => P (T(P)) and for every predicate P,Q we have (forall x, P(x) <=> Q(x)) => T(P) = T(Q); it is a conservative extension of ZFC who satisfy the same arithmetical sentences as ZF anyways, by working into the constructible universe of the former).
- Russell's iota definition operator is just T restricted to predicates satisfied by an unique element.
-"A union B":= T (x -> forall t, t is in x <=> (t is in A or t is in B)).
Simple data types:
- S(x) is an abbreviation of x union {x}
"n is an integer" is an abbreviation of "forall X, (emptyset is in X) => (forall y, y is in X => S(y) is in X" => n is in X".
"{a,b}":= T(x -> forall y, (y = a \/ y = b) <=> y is in x)"
"(a,b)":= {{a},{a,b}}
"f is a function":= (forall a b c, ((a,b) and (a,c) are in f => b = c)) and for every x in f there are y,z such that x = (y,z)
"dom(f)":= T(x -> forall z, z in x <=> exists t, (x,t) is in f )
"f is a list":= f is a function and dom(f) is an integer
"A x B":= T(x -> forall t, t is in x <=> exists a b, t = (a,b) and a is in A and b is in B)
"M is an array of size (A,B)" := M is a function and dom(M) = A x B (A, B are often integers)
"X is a tree":= every member of X is a list and for every integer n and f in X such that dom(f) = S(n), there exists g in X and there exists p such that dim(g) = n and f = the union of g and (S(n), p).
"X is a decorated tree":= X is a function and dom(X) is a tree.
Anonymous at Thu, 3 Apr 2025 17:44:10 UTC No. 16636244
>>16636026
You have never studied set theory.
Anonymous at Thu, 3 Apr 2025 18:48:28 UTC No. 16636321
>>16636228
Yes, set theory and type theory can both interpret each other. Type theory is the one that's more easily mechanizable though.
Encoding mathematical structures into set theory produces way more garbage theorems that are due to the encoding rather than due to the structure than doing the same in type theory does.
>>16636244
You have studied neither.
Anonymous at Thu, 3 Apr 2025 19:04:23 UTC No. 16636344
>>16636321
>You have studied neither.
I know more set theory than you ever will.
>set theory produces way more garbage theorems
>garbage theorems
Fuck off lmao. This bullshit is so stupid. You're garbage, not set theory. Yes, 2 is a member of 3. Deal with it.
Anonymous at Thu, 3 Apr 2025 19:19:02 UTC No. 16636359
>>16636321
>Encoding mathematical structures into set theory produces way more garbage theorems that are due to the encoding rather than due to the structure than doing the same in type theory does.
Encoding the rational numbers ordered pairs [math]a/b=(a,b)[/math] already raises annoying complications. Making [math]\mathbb Q[/math] primitive as in some type theories is just passing the buck, since you have a whole new kind of problem at [math]\mathbb R[/math] that primitive [math]\mathbb N, \mathbb Q[/math] don’t help with at all, and then topology, geometry and measure theory are another level beyond that
But yeah I guess at least you don’t have [math]\max(m,n) = m \cup n[/math] if you were really bothered by that
Anonymous at Thu, 3 Apr 2025 19:37:02 UTC No. 16636382
>>16636359
No type theory makes rationals primitive, what are you smoking? Quotients are better behaved in type theory than ordered pairs will ever be in ZFC, and that's without taking into account HIITs from HoTT OR extensionality.
No one takes foundations seriously because it's synonymous with that sort of pointless set theoretical mental gymnastics. Even the most basic bitch intensional type theory is closer to the pragmatics of actual mathematicians than material set theory is.
Anonymous at Fri, 4 Apr 2025 09:15:39 UTC No. 16637109
>>16636321
>garbage theorems
How is that even a concern?
Will you throw away a programming language just because it could (also) allow you to quickly write a program displaying "I'm a faggot" 1 billion times on your screen?
He who can do more can do less....
Anonymous at Fri, 4 Apr 2025 09:48:10 UTC No. 16637116
set theory=C
HTT=rust
type theory=?
category theory=?
Anonymous at Fri, 4 Apr 2025 10:17:42 UTC No. 16637135
>>16637109
No, but I will throw away a programming language because it allows you to quickly shoot yourself in the foot. Also, there's no "he" in this analogy, set theory is a tool, not a person. You don't use a hammer with a kitchen sink chained to its handle to hammer a nail, you just use a hammer. Less is more.
Garbage theorems hinder mechanization and tooling. Actual mathematics is so far removed from its set theoretical encoding that it makes you wonder why care about having foundations at all other than the curiosity that "it's possible". It's a joke. Type theory has actual practical applications as a foundation.
Anonymous at Fri, 4 Apr 2025 11:16:07 UTC No. 16637172
>>16637116
Coq is in there
Anonymous at Fri, 4 Apr 2025 11:28:18 UTC No. 16637180
>>16637172
Coq is a fine tool, don't get me wrong but...
For a good laugh ask yourself in what kind of "weak" theory it has been proven that every program written in Coq terminates (last time I've checked it was ZF+ there is a countable set of inaccessible cardinals)?
For the record Coq proves that classical second order arithmetic (with full comprehension scheme which is quite strong already) is consistent, and even does witness extraction for sigma1 and pi2 formula (using Harvey Friedman A-translation method for converting a proof of such a formula into an intuitionistic one and completing with an Acc based trick to convert a proof of "exists x: nat, P x" into a term of type {x: nat | P x} when P is decidable by a boolean function).