@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

@aescling …lean?

@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

@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

@aescling @Lady is lady trying to convince you that math is useless again

@wallhackio @aescling i don’t think math is useless i just think it is a humanities

@Lady @aescling ?

@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

@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”