I'd be very interested to know more about your music typesetting. FWIW, my tool of choice is PMW. Like Lilypond it takes textual input; unlike Lilypond its input language is reasonably lightweight; perhaps there is some highly formulaic and repetitive music for which the procedural stuff Lilypond can do is actually useful, but I don't think I've ever seen a case where it would be worth the overhead.
What was the theorem, and how hard was it to prove?
Ah yes, PMW was mentioned to me but I never quite got round to looking at it. It looks to be on roughly the same general level of complexity as Mus (my own unpublished effort as mentioned above). A brief look at its font in particular doesn't do anything to make me think I've been wasting my time, though :-)
The theorem: given a positive integer n, how many integers do you need in order to guarantee that n of them sum to a multiple of n? (answer and five different proofs) I think it took us about an afternoon or so of serious thought between us to find a proof, once we'd decided what we thought the right answer was to start with (for which I cheated by computer search). Of the five proofs given there, ours was pretty similar to the first one (though Erdős's version, as one might expect, was more elegant and included a more neatly reusable lemma).
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
What was the theorem, and how hard was it to prove?
The theorem: given a positive integer n, how many integers do you need in order to guarantee that n of them sum to a multiple of n? (answer and five different proofs) I think it took us about an afternoon or so of serious thought between us to find a proof, once we'd decided what we thought the right answer was to start with (for which I cheated by computer search). Of the five proofs given there, ours was pretty similar to the first one (though Erdős's version, as one might expect, was more elegant and included a more neatly reusable lemma).