Morgan Arnold

one thing that's been on my mind is the role of proof assistants. @johncarlosbaez started a great thread a week or so ago about the role of formalisation in mathematics. martin escardo said something in that thread that stuck with me, basically talking about using proof assistants as a tool of thought. like any tool of thought, i think that it's important to understand that any proof assistant will necessarily have limits to its expressive capabilities, or design decisions which demand that thought be laid out in a certain way, and that mathematical thought does not have to fit within the box of the expressive capabilities of any proof assistant to be valid, worthwhile mathematical thought

@TeaKayB it hasn't been released yet, but there's a guy building an open hardware ereader which seems pretty awesome: https://www.crowdsupply.com/oddly-specific-objects/open-book-touch

@leftpaddotpy@hachyderm.io out of curiosity, what do you mean when you say that people can't choose the things that they see? i'm not sure what the "normal" way to use fedi is, but i only really look at my home feed, so i only see stuff from people i follow. i mostly follow personal friends, and sometimes they boost other interesting people into my feed who i decide to follow. if i consistently dislike someone's posts, i just unfollow them.

as an example, i had a very interesting discussion on irc the other day about the relationship between total orders and decidable orders. if you define totality in the "obvious" way, as \((x\ y : S) \to x \le y \uplus y \le x\), this turns out to be equivalent to decidability of the order (better still, the proof is surprisingly tricky)! to distinguish the two notions, you need to be sure that totality is valued in propositions, and define it as something like \((x\ y : S) \to \| x\le y \uplus y \le x \|\). it's a neat bit of subtlety which simply disappears classically

@chrisamaphone i didn't really notice just how slowly i process things until i had to take oral exams during my master's degree, where an inability to think quickly in front of others is punished quite harshly. i do absolutely find value in being a relatively slower thinker. i get a lot out of ruminating on things for a long time

for instance, ink on paper has been the primary tool for the expression of mathematical thought for a very long time, but this tends to impose a kind of linearity to the expression of thought. think of all of the textbooks which begin with a kind of "dependency graph," showing which chapters of the book depend on the contents of which other chapters. this is a kind of kludge to get around the limitations of the tool of thought being used! there are projects, like amélia liao's venerable 1lab, which use hypertext instead of ink on paper! hypertext gets around this particular limitation of paper as a tool of thought, but of course it has its own limitations!

i suppose that the point that i'm trying to make is that mathematical thought necessarily transcends any particular medium for its expression, and need not conform to the limitations of any particular medium for it to be valid and worthwhile. a diverse proliferation of tools of thought therefore seems vastly preferable to the evolution of a consensus in which one way is thought of as being "the right way"

@alisonkiddle@mathstodon.xyz the probability of the coins is, as others have noted, just 1/2¹⁰, and the probability of the dice is 1/6⁴. now, i want to know which of 2¹⁰ and 6⁴ is larger. first, note that 6⁴ = 2⁴3⁴, so i just need to know which of 2⁶ and 3⁴ is larger. then, i observed that since √2 ≈ 1.4, this means that 2√2 < 3, but (2√2)⁴ = 2⁶, ergo 2⁶ < 3⁴, and the coin flips are likelier! this seems to be a more circuitous route than some other people have taken, but it was fun to do it in a way that doesn't require any mental multiplication or knowing a bunch of powers off the top of your head, especially since i have a terrible memory for that sort of thing

@megalomaniac you could potentially run into issues with the lack of the play integrity api causing apps to not work, although in ~4 years of using graphene, the only app that has ever absolutely refused to work for me was, bizarrely, the eurovision ticketing app

@jonmsterling i'm curious why you think that this is at least a factor in democratically-organised open source non-viable. you not that a project could (and indeed, in your view should) simply democratically decide not to allow contributions from llms. is your opinion that this represents some kind of unstable equilibrium?

@jonmsterling these decisions might indeed fracture communities, although internal debates fracturing open source communities is nothing new. i'm not totally sold on the idea that the debate will come up over and over again, however. assuming that the community does indeed split, you now have one community which falls on one side of the debate, and one which falls on the other. those don't seem to me like environments in which that debate would continue for instance, i can't imagine that a "no llms" fork of some project would continue to have internal debates over contributions from llms, precisely because that is now a community which consists of people who were on board with a "no llms" fork in the first place!

@jacqueline hi jacquelines i'm writing a blog post