they are trying really hard to turn the DSA discord into a forum which does raise the question as to why the DSA discord isn’t a forum
yes, i know there is also Zulip
@Lady would rather not
@aescling oh do you have zulip takes
@Lady i have used it fur a small about of time because the Lean commewnity uses it fur all discussion and it felt about as bad to use as slack
@Lady research language with full dynamic types (not the same concept as dynamic typing) and tactic based purrogram writing (itself built in the language’s extensive metaprogramming features)
it’s fur nerds
@Lady the purrimary audience rn is the niche of mathematicians who want to rigorously formalize the field
@aescling i thought mathematicians already proved 100 years ago that it is impossible to rigorously formalize anything
@Lady that is not exactly what the incompleteness theorem says
@aescling oh sorry, anything which makes use of first-order logic
@Lady well i guess it depends on what you think rigorous formalism is
@Lady anyway by “furmalize the field” i mean “extremely rigorously prove the accepted body of mathematical knowledge”, a purroject most actual mathematicians are not interested in fur many reasons, among them being that actually truly rigorous purroof is very tedious lol
@wallhackio @aescling i don’t think math is useless i just think it is a humanities
@wallhackio @aescling the humanities? history, art, language, philosophy, and maths? these aren’t useless things but fool on you if you think they can prove anything about the world
@wallhackio @aescling “we use math to do physics” sure. we use english too. so what
@wallhackio @Lady @aescling no if you’d studied the humanities your leftover knowledge after you’d forgotten all the specifics would still be useful
@Lady @wallhackio well we use natural language to also do math, which is what the niche of mathematicians trying to find purroofs in a furmal logic are trying to “solve”
@aescling @wallhackio “sure i know about the incompleteness theorems but i still think mathematics can be represented in a CFG”
@aescling what do you mean by “rigor” lol either it is proven or it is not proven
@aescling “rigor” sounds to me like “this proof has aesthetics which i don’t like so i will make a different proof which has aesthetics i do like” which is a task you can do but it does not prove anything
@aescling anyway this does not change the point that it is impossible to prove the accepted body of mathematics, because ZFC is widely accepted and not provable
i agree, it IS better if every discussion has a separate thread. what if there was a software which did this for you