joppy

The university just needs to set an assignment which needs to be submitted twice: once with citation style A, and again with citation style B. Anyone not using citation management software will quickly start.

The text dims a bit too fast to read comfortably on my phone (especially since in the latest version of iOS Apple has inexplicably moved the address bar from the top of the screen to the bottom).

But this scrolling paradigm is just fantastic for looking through the CT scans on my phone - I can easily move up and down layers. Kudos to the web design.

If my intent is that a certain integer should never be negative, labelling it unsigned does a poor job at conveying this intent because any arithmetic just silently does the wrong thing. 3-4 is some huge number rather than “error”.

> I adjusted my headlamps down…

I was told that the headlight adjustment in some large vehicles are meant to accomodate for weight (2 people in front vs 5 people in vehicle), but it seems that most people simply adjust this as high as it goes because they can see further. Even in Australia, which doesn’t have quite as much of a large-car problem, it’s becoming incredibly difficult to drive on the highway at night in a small car due to incredibly bright lights from behind.

I think this is a good policy, and have often been annoyed that I can’t (rules of the university) mark my students down for such absurd answers.

This is the same as my experience growing up in Australia - right the way from primary school up to university-level subjects, mathematics working is marked and you get almost full points if you solve the problem correctly but just make some clerical error somewhere. Even if you can show progress towards a solution but can’t quite get the last bit, you’ll often get 7 or 8 out of 10.

This isn’t a free marketplace of ideas though - thanks to dubious algorithms and recommendations, not all ideas even have a chance of being seen, let alone the bad ones buried. The echo-chamber phenomenon is like walking into a shop, looking at an item on a shelf from one manufacturer, and then once you put it back and look around you can only see items from that manufacturer. You get trapped in a bubble where you’re only ever seeing content like the content you just engaged with.

I agree that in a free marketplace of ideas bullshit content would get buried, but this isn’t how modern social media platforms work.

You might have an abstract function f which takes and returns an integer, and you want to figure out if this function has “cycles”, eg if ffffff(n) = fff(n) etc. The numbers used might be enormous, and so trying to store them all is a non-starter.

Yeah you're totally right, my bad.

> If you have a set with two binary operations, then a monoid isn't the correct abstraction.

I guess my point is that even if I used "the correct abstraction" here, meaning a ring or something, then the whole newtype setup still makes it annoying for me to split off one operation and feed it into a function expecting a monoid: the way that fold and friends work is much more natural, just taking a starting value 1 and an operation * for example, rather than some kind of "Multiplicative" newtype or whatever.

In general I see a lot of the abstract algebra type towers in Haskell and Purescript as being unhelpful, and making a huge assumption that (for example) there will rarely be two monoid instances on a type. In reality in abstract algebra we use tons of different operations on the same objects all the time, and I really just want to define those operations and then be able to use them.

What's wrong with newtypes is that if you want to define "the monoid of integers under addition" and "the monoid of integers under multiplication" (or similar, the second isn't really a monoid because of zero), then an expression like a*x+b becomes some kind of newtype hell:

toAdditive ((toMultiplicative a) <> (toMultiplicative x)) <> toAdditive b

or something similar. This is of course an insane way to program, and so really what is done is that we define two entirely different operations of addition and multiplication so that they can be used without newtypes.

What would be cool is if operations could ad-hoc be bound to instances of typeclasses, for instance you could accumulate a list of integers inside the (0, +) monoid, or inside the (1, *) monoid. Of course this is basically what the fold functions in Haskell do, but you could imagine being able to formalise this pattern at the type level in a less newtype-hellish way.

Rotation matrices are still ubiquitous even in systems which use quaternions: if you want to apply a dense linear transformation to a vector (be it a rotation or otherwise), pretty much nothing will beat (in terms of speed) a matrix-vector multiplication. For instance even if you work out the rotation matrices using quaternions, an engine will end up shipping a rotation matrix to a graphics card to actually transform the bulk of vertices in a scene.

Quaternions are the even part of the Clifford (aka Geometric) algebra associated to a three-dimensional space, so the connection is quite close. This case is also quite special because the quaternions form a division algebra over the real numbers, meaning that each nonzero quaternion has an inverse. Finite-dimensional real division algebras are quite rare: indeed the only ones up to isomorphism are the real numbers, complex numbers, and quaternions.

Geometric algebra is great if you want to extend things to higher dimensions, or spaces with different metric signatures (the 4-dimensional spacetime for example). But quaternions should not be discounted just because they fit into a generalisation - they have many quite special properties all of their own.

This question seems to always come up on Hacker News - figuring out how to even formulate the statement of theorems in theorem provers such as Lean is a massive research undertaking in itself, requiring much creativity and novel work. Let alone figuring out how to formulate the proofs. I’d recommend you have a look at some of the talks that Buzzard has given on this to understand the complications (both technical and social) and progress that has been made so far.

It’s more like “in a world where every group of n horses are the same colour”, no matter of whether that world is the real world or not, “prove that any group of n+1 horses are the same colour”. This inductive step proves nothing about the real world, it needs a base case to kick things off. If you can prove it true for n=5 say, then the inductive step gives you every higher number.

This is standard induction: let P(n) be some statement about the number n. If you can establish that P(n) implies P(n+1) for all n >= 1, and that P(1) is true, then P must be true for every positive integer. You can find many examples by googling for “induction proof”.

The problem in the proof is that the inductive step P(n) implies P(n+1) only holds for n >= 3, and so the fact that P(1) is true does not imply anything for the larger integers.

I heard from a friend (have not verified myself) that the paper in which the Magma computer algebra system was introduced is the most-cited paper in the whole of pure mathematics.

Groups are not inherently discrete - there are many continuous groups (called Lie groups) such as the circle, group of rotations in 3D, etc etc. You can also see this turn up in Fourier theory: the discrete Fourier transform has an underlying discrete group, Fourier series for a periodic function are really using the circle group underneath, and the Fourier transform on the real line is using the continuous group of the real line, with addition as the group operation.

Elliptic curves are nice because they are algebraic groups, so by plugging in complex or real numbers you get a continuous group, and by plugging in finite fields you get a discrete group.

What? The mathematics shows correctly on the page for me, and that PDF is missing some chessboard images...

Trying to stylise the letter M to be distinctive is pretty circuitous - just use an icon of a train! You remove the problem almost entirely, and get a symbol which is easily recognisable even to people who don’t speak the local language.

In Sydney, in the last 10 years our icons have been replaced by stylised letters. T stands for train (not Taxi or Tram), except when it doesn’t and M stands for Metro (which everyone still just calls the train), L stands for light rail (which everyone calls Trams)… it was so much more clear when there were just icons.

Things fail in the weirdest ways in unsupported environments though, it’s not like the “make transfer” button doesn’t work, it’s more like it might not even show up in the first place. Having 99% of your website work and the last 1% not work is a dealbreaker in many cases, and these “the site may not work for you based on your OS” banners lead the user into thinking it does work 100% if it works in 99% of the cases.

Not saying this is the way it should be, just saying that “doing your best” to allow unsupported platforms often leads to a terrible and confusing user experience.

Because Svelte can look through the template, and at compile-time determine exactly which parts of the output need to be "surgically updated" in the DOM when some of the inputs change, without needing any runtime like a virtual DOM implementation. I don't know how you could implement such a thing (with good ergonomics) without a template language.

I think that software like mathematica is a great tool, and anyone genuinely doing research that would benefit from it should be happy to pay for it as a matter of course. But I can also see many of the downsides to using closed-source software for research (I myself use some, not mathematica but related) - you don’t know what algorithms are being used, and can’t check yourself that they do what you expect, or fix them if they go wrong. For truly research-level questions, checking that an algorithm produces the correct output may be as hard as writing the algorithm itself…

It’s universal portability, but at the cost of only using the lowest-common-denominator features of any random markdown implementation. There are so so many more things that can be done with websites and long-form writing than big standard markdown, and even Pandoc (which I consider to be the most versatile fully-featured markdown implementation) has extensive support for user-written filters, which provide more on top of what Pandoc markdown provides.

What is the priority - being able to switch blog implementations at the drop of a hat, or having an actually good website?

I feel the same way - if computers happened to use base 3 instead of base 2 we could have fixed-width signed integers which are symmetric about zero.

Trivial, or just straightforward? I don’t think that it’s trivial to know why multiplying by this powers-of-roots-of-unity matrix is interesting, and does the things that it does.

The post itself shows that it is non-trivial to even boot this hardware with Nix.

JavaScript is a language where you need to implement your own hash table, since the built-in object only understands key strings, and the built-in Map class only has value semantics when the keys are primitive types (strings, ints, etc), and compares objects by object identity.

Is microseconds correct? Even with a good connection in online games I’ve only seen ping latencies of 3ms or so, and a more common range on an average connection is 20ms-50ms.

Whatever the case, what you end up with is an asset whose actual value is tied to the interest rate (interest goes down, people can afford larger loans with the same repayments, therefore houses are worth more). This is a highly leveraged situation: if you take out a $1m loan and then interest rates go up, you're still liable for the whole $1m even though your actual asset might only be worth $900k now. I think this is one of the big dangers of having an essential need like housing cost such a large multiple of income.