@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

@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

@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 @aescling as a recovering physicist most of my physics knowledge is completely useless so i guess i studied a humanities

@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 @aescling @wallhackio thats why the liberal arts model makes everyone study the humanities regardless of major

@Satsuma @wallhackio @Lady he did end up with some useful takeaways from a religion class he had to take

@Satsuma @wallhackio @Lady @aescling empecé a decir que la secuencia de humanidades obligatoria que cursaba no me sirve para nada más que saber las respuestas de programas de quiz. pero me acordé de que el leer de las memorias de nabokov me dio una desconfianza fuerte de escritores buenes. también aprendí que Aquinas no tenía buena lógica. y que algunos hombres str8 cogen a otros hombres. resulta que me quedan muchos conocimientos útiles de esos cursos.

@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 @wallhackio anyway if they think proofs that prove mathematics for humans are insufficient i am curious what other audience for their mathematics they are imagining

@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