Martin Escardo@MartinEscardo@mathstodon.xyz
The "mute" feature is very useful when somebody bombards a thread.
Is there a way to mute somebody only from a specific thread, rather than all their posts, @FediTips@social.growyourown.services ?
Martin Escardo@MartinEscardo@mathstodon.xyz
Martin Escardo@MartinEscardo@mathstodon.xyz
Martin Escardo@MartinEscardo@mathstodon.xyz
Mathematicians: What are the important definitions in your field?
For example, in topology the notions of compactness and of Hausdorff space are crucial (among many others).
Or in complexity theory the notion of NP-completeness.
And so on.
Can you list the ones in your mathematical field?
Non-practicing-mathematicians: this time just listen what the practicing mathematicians say.
This is an exercise, for me, in learning which concepts working mathematicians of fields different from mine consider to be important for their own field.
PS. I will consider Theoretical Computer Scientists and Theoretical Physicists for this question. And I am also willing to be more general, without any specific example in mind.
Martin Escardo@MartinEscardo@mathstodon.xyz
@johncarlosbaez@mathstodon.xyz @j_bertolotti@mathstodon.xyz @julesh@mathstodon.xyz
The analogy with automatic transmission is not very good, as it generally works safely, whereas "vibe coding" with genAI doesn't generally work safely, and often fails badly (with many examples reported by the press and some in court for releasing private information as a result of not implementing any security measure, for example).
Martin Escardo@MartinEscardo@mathstodon.xyz
@johncarlosbaez@mathstodon.xyz @j_bertolotti@mathstodon.xyz @julesh@mathstodon.xyz
If you allow me, let me say more about this (which I would not regard as original thinking).
The problem with genAI is that there is no specification given to the general public of what it actually does, not even an informal one, that can be verified empirically or mathematically.
What happens now is that you ask a question to chatSomething, and then it gives an answer. Is the answer correct? Sometimes. And often not, and the frequency of (in)correctness depends on the subject (programming, cooking, molecular biology, mathematics, counselling, law, whatever).
Can this work in the future? Maybe. People are very creative, and may make this work. After all, many of us believe that intelligence, like everything else in nature, is ultimately mechanical.
But right now we get an answer with no promise of correctness, not even in a very vague sense of correctness.
We get answers with no promises that they answer the question, and worse, often they don't answer the question correctly for questions we already know the answer.
Never mind the questions for which nobody knows the answer (or that just the person asking the question doesn't know the answer).
Martin Escardo@MartinEscardo@mathstodon.xyz
I was considering creating my own blog, but I am instead happy to post here or occasionally at @andrejbauer@mathstodon.xyz 's blog Mathematics and Computation.
For easy access, though, I've created a web page that indexes my posts, which, with luck, will itself be indexed by search engines:
https://www.cs.bham.ac.uk/~mhe/blog.html
Martin Escardo@MartinEscardo@mathstodon.xyz
Index of selected threads on #hott #constructive #math
* 2022/10/31. Proofs by contradiction.
https://mathstodon.xyz/@MartinEscardo/109264034964990196
* 2022/11/12. Synthetic topology of data types and classical spaces.
https://mathstodon.xyz/@MartinEscardo/109332986014534390
* 2022/11/14. Notions of space.
https://mathstodon.xyz/@MartinEscardo/109343930842850773
* 2022/11/16. Trichotomy of ordinals.
https://mathstodon.xyz/@MartinEscardo/109355604029879269
* 2022/11/22. Birthday present by Tom de Jong.
https://mathstodon.xyz/@MartinEscardo/109388875794058555
* 2022/11/23. Concrete example illustrating that constructive mathematics is more general than classical mathematics.
https://mathstodon.xyz/@MartinEscardo/109395006766077334
* 2022/12/01. Combinatorial game theory.
https://mathstodon.xyz/@MartinEscardo/109440314312765877
* 2022/12/08. Universe polymorphic type systems.
https://mathstodon.xyz/@MartinEscardo/109480057029596732
* 2022/12/08. Why cubical type theory, and why cubical Agda?
https://mathstodon.xyz/@MartinEscardo/109480455436886869
* 2022/12/20. The axiom of choice in HoTT/UF.
https://mathstodon.xyz/@MartinEscardo/109546988519874380
* 2022/12/22. A common generalization of the univalence axiom and the K axiom.
https://mathstodon.xyz/@MartinEscardo/109558670025171863
* 2023/02/03. Defining large numbers without using induction.
https://mathstodon.xyz/@MartinEscardo/109802885041067972
* 2023/02/10. Several kinds of categories in HoTT/UF.
https://mathstodon.xyz/@MartinEscardo/109842791175514936
* 2023/03/03. Universes in type theory as mathematical objects interesting in their own right.
https://mathstodon.xyz/@MartinEscardo/109961534132268566
* 2023/03/22. Playing rationally against irrational players.
https://mathstodon.xyz/@MartinEscardo/110068977445045121
* 2023/04/11. What are universes for in HoTT/UF?
https://mathstodon.xyz/@MartinEscardo/110181596099423100
* 2023/06/02. Ayberk's predicative version of the patch locale of a Stone locale.
https://mathstodon.xyz/@MartinEscardo/110476555405397697
* 2023/06/07. Github project TypeTopology.
https://mathstodon.xyz/@MartinEscardo/110504563233350460
* 2023/06/15. Constructive notions of disjunction.
https://mathstodon.xyz/@MartinEscardo/110549967500023998
* 2023/07/09. Trichotomy of the reals constructively.
https://mathstodon.xyz/@MartinEscardo/110685074921103237
1/