@byorgey@mathstodon.xyz

Brent Yorgey @byorgey@mathstodon.xyz · Jun 06, 2026

Replying to @RuchiraSDatta@mathstodon.xyz

@RuchiraSDatta@mathstodon.xyz It works for me. It's just a static site that doesn't implement HTTPS, so your browser may object if it insists on toxic max-security. https://www.youtube.com/watch?v=M1si1y5lvkk

1

2

0

Brent Yorgey @byorgey@mathstodon.xyz · Jun 06, 2026

Replying to @lindsey@recurse.social

@lindsey@recurse.social aww, thanks!

3

2

0

Brent Yorgey @byorgey@mathstodon.xyz · May 29, 2026

Replying to @koronkebitch@types.pl

@plragde@mstdn.social @koronkebitch@types.pl Agreed on both counts!

0

Brent Yorgey @byorgey@mathstodon.xyz · May 29, 2026

Replying to @koronkebitch@types.pl

@plragde@mstdn.social @koronkebitch@types.pl I don't doubt your experience. I am just saying that there do exist institutions that actually do prize teaching, where doing a barely competent job on teaching while prioritizing research would not get you very far. I work at one of them.

0

1

0

Brent Yorgey @byorgey@mathstodon.xyz · May 28, 2026

Replying to @koronkebitch@types.pl

@plragde@mstdn.social @koronkebitch@types.pl Teaching does count for hiring, tenure, and promotion at some institutions (the best ones)!

1

0

Brent Yorgey @byorgey@mathstodon.xyz · May 11, 2026

I was testing out a Swarm scenario that starts by generating a random permutation of characters. I ran it and this is the first random permutation that was generated. 👻 😱

8

1

0

Brent Yorgey @byorgey@mathstodon.xyz · May 11, 2026

Replying to @jer_gib@functional.cafe

@jer_gib@functional.cafe Thanks! I'll definitely need to spend some time digesting this. Hopefully I can package everything into a nice blog post next week.

2

0

Brent Yorgey @byorgey@mathstodon.xyz · May 11, 2026

Replying to @oantolin@mathstodon.xyz

@oantolin@mathstodon.xyz @das_g@chaos.social Yeah, the reversing thing is an artifact from the way I was initially thinking about it. I agree with you.

0

Brent Yorgey @byorgey@mathstodon.xyz · May 11, 2026

Replying to @oantolin@mathstodon.xyz

@oantolin@mathstodon.xyz Yep! This is essentially the solution that @das_g@chaos.social posted: https://chaos.social/@das_g/116547298268126736

1

2

0

Brent Yorgey @byorgey@mathstodon.xyz · May 10, 2026

Replying to @byorgey@mathstodon.xyz

Aha, I think it must have something to do with the bijection between encodings of integer partitions as (1) nonincreasing lists of natural numbers and (2) arbitrary lists of natural numbers, witnessed by sending a nondecreasing list to its list of successive differences. For example, the partition [6,6,4,3] corresponds to [0,2,1,3]. (6 - 6 = 0, 6 - 4 = 2, etc.) I'm quite sure I have seen this bijection exploited before, perhaps in Richard Bird's book Pearls of Functional Algorithm Design? I'll have to look once I get back to my office tomorrow.

2

4

1

0

Brent Yorgey @byorgey@mathstodon.xyz · May 10, 2026

Replying to @byorgey@mathstodon.xyz

So far I've managed to prove that

map length . transpose . map (replicate ()) = foldr (\n -> zipWithExt (+) 0 (replicate n 1)) []

where

zipWithExt :: (a -> a -> b) -> a -> [a] -> [a] -> [b]

zips the lists together with the given function, using the provided value of type a to fill in missing values from the shorter list.

This is very similar to @oantolin@mathstodon.xyz 's implementation, and does indeed get rid of the unit values, but it turns out the unit values themselves weren't the problem: the real problem is that we want to avoid the use of replicate to encode Int values in unary. This version with foldr is still O(sum p), i.e. linear in the total size of the partition, but we want an implementation which is O(length p + maximum p), i.e. linear in the number of parts plus the size of the maximum part. I think my fiddly directly recursive implementation achieves that, as does @das_g@chaos.social 's implementation, but I want to figure out a way to derive those from the direct specification.

5

13

2

0

Brent Yorgey @byorgey@mathstodon.xyz · May 10, 2026

Replying to @jer_gib@functional.cafe

@jer_gib@functional.cafe More concretely, what's the nicest way you know of to define transpose? The actual implementation in the Haskell standard library is gross. The best I've come up with is

transpose = foldr (zipWithExt (++) . map pure) []

where zipWithExt :: (a -> a -> a) -> [a] -> [a] -> [a] is the analogue of zipWith which extends to the longer of its two list arguments instead of truncating to the shorter.

0

9

0

Brent Yorgey @byorgey@mathstodon.xyz · May 10, 2026

Replying to @liamoc@types.pl

@liamoc@types.pl @jonmsterling@mathstodon.xyz Thanks, agreed! I enjoy reading both of yours for similar reasons.

0

Brent Yorgey @byorgey@mathstodon.xyz · May 09, 2026

Replying to @das_g@chaos.social

@das_g@chaos.social Oh, that's very nice! I'm pretty sure that is behaviorally very close to my version, but implemented in a much nicer style.

0

Brent Yorgey @byorgey@mathstodon.xyz · May 09, 2026

Replying to @das_g@chaos.social

@das_g@chaos.social Yeah, the actual implementation is kind of gross because it's trying to be efficient and have nice strictness properties and whatnot. There's probably a much simpler definition...

0

Brent Yorgey @byorgey@mathstodon.xyz · May 09, 2026

Replying to @byorgey@mathstodon.xyz

Incidentally, if anyone wants to play with this, here's my fiddly but efficient version:

conjugatePartition :: [Int] -> [Int]
conjugatePartition ps = go (length ps) 0 ps
 where
  go :: Int -> Int -> [Int] -> [Int]
  go !r !l [] = []
  go !r !l ps@(p : _) = replicate (p - l) r ++ go (r - length pre) p rest
   where
    (pre, rest) = span (== p) ps

2

3

0

Brent Yorgey @byorgey@mathstodon.xyz · May 09, 2026

Replying to @byorgey@mathstodon.xyz

I guess the idea would be to expand the definition of transpose and then start commuting/fusing the map length and map (replicate ()) with things until they "cancel out" and there are no unit values left anywhere in the computation.

1

20

0

Brent Yorgey @byorgey@mathstodon.xyz · May 09, 2026

I wanted a #Haskell function to efficiently compute the conjugate of an integer partition. I think I know how to write it, but it's fiddly. There's a nice, succinct functional specification:

conjugate = reverse . map length . transpose . map (`replicate` ())

but it's slow. Now I'm wondering whether it's possible to derive an efficient version from this specification, #Bird-Meertens style. Anyone know of previous work along these lines? Or should I add it to my list of interesting projects?

12

36

2

0

Brent Yorgey @byorgey@mathstodon.xyz · May 07, 2026

Replying to @oantolin@mathstodon.xyz

@oantolin@mathstodon.xyz Hah! I think this job is mostly asbestos-free. Though there are some kind of old buildings.

0

Brent Yorgey @byorgey@mathstodon.xyz · May 07, 2026

Replying to @oantolin@mathstodon.xyz

@oantolin@mathstodon.xyz I don't have any specific examples at hand, but my impression is yes, with varying values of "forcing".

0

3

0

Brent Yorgey @byorgey@mathstodon.xyz · May 07, 2026

My department is hiring a 1-year visitor in mathematics. Please pass along to anyone you know who might be interested - this is a really fantastic place to work, with engaged students, supportive colleagues, and no one forcing you to use LLMs for anything. https://hcm.paycor.com/l/r/D555BCF0

7

34

0

Brent Yorgey @byorgey@mathstodon.xyz · Apr 30, 2026

Replying to @maxsnew@types.pl

@maxsnew wow, congrats!!

2

0

Brent Yorgey @byorgey@mathstodon.xyz · Apr 28, 2026

Replying to @riley@toot.cat

@riley I appreciate you defending me (though for the record I did not feel attacked by @leonardom 's post), but please let's not call each other names.

1

0

Brent Yorgey @byorgey@mathstodon.xyz · Apr 27, 2026

I wrote something for my students reflecting on the current cultural and technological moment - a collection of important things I want to say that I'm never quite sure how or when to say in class.

http://ozark.hendrix.edu/~yorgey/forest/00FD/index.xml

ozark.hendrix.edu

150

24

129

2

Brent Yorgey @byorgey@mathstodon.xyz · Apr 27, 2026

Replying to @alp@mathstodon.xyz

@alp@mathstodon.xyz Hah! Maybe it's because my website serves only http, not https? Or because your browser considers anything a security risk if it has an unknown extension?

0

1

0

Brent Yorgey @byorgey@mathstodon.xyz · Apr 25, 2026

Replying to @byorgey@mathstodon.xyz

@MartinEscardo@mathstodon.xyz It's now publicly available from http://ozark.hendrix.edu/~yorgey/pub/FTA.agda .

0

1

0

Brent Yorgey @byorgey@mathstodon.xyz · Apr 24, 2026

Replying to @JacquesC2@types.pl

@JacquesC2 @maxsnew I was gonna say the same thing. Re-learn algebra yes, but not for those reasons.

3

0

Brent Yorgey @byorgey@mathstodon.xyz · Apr 22, 2026

Replying to @Taneb@hacksrus.xyz

@Taneb@hacksrus.xyz Oh, did you make that? Nice! I didn't look at it while I was writing mine, but I did find it to compare once I was finished. The proofs are pretty similar in broad outlines, as one might expect, but yours is definitely more efficient: for example, to test whether a number has a factor I simply try every possible divisor less than it; my proof makes no attempt to stop when reaching the square root, as yours does.

1

0

Brent Yorgey @byorgey@mathstodon.xyz · Apr 21, 2026

Replying to @MartinEscardo@mathstodon.xyz

@MartinEscardo@mathstodon.xyz It's currently in a private repository full of experiments and solutions to competitive programming problems that I don't want to make public, but I will copy it somewhere public soon.

1

0

Brent Yorgey @byorgey@mathstodon.xyz · Apr 21, 2026

Replying to @boarders@mathstodon.xyz

@boarders@mathstodon.xyz oh, I think the Fundamental Theorem of Algebra could be proved in 750 lines of Agda. Some of the lines might be a bit long though.

4

0

Brent Yorgey @byorgey@mathstodon.xyz · Apr 21, 2026

Replying to @boarders@mathstodon.xyz

@boarders@mathstodon.xyz I was like, what, real numbers?? Then I realized I accidentally said the Fundamental Theorem of *Algebra* when I actually meant *Arithmetic*! haha, oops!

8

2

0

Brent Yorgey @byorgey@mathstodon.xyz · Apr 21, 2026

Finally finished a just-for-fun, completely-from-scratch constructive proof of the Fundamental Theorem of Arithmetic (just the existence part, not uniqueness (yet)) in #Agda. Took me about 10 hours and 750 lines of code. Fun times! Will probably turn it into a blog post at some point.

34

14

7

0

Brent Yorgey @byorgey@mathstodon.xyz · Apr 21, 2026

Replying to @peterrowlett@mathstodon.xyz

@peterrowlett @robinhouston Yes, but probably not a formally specified one. Everyone is afraid of zero.

0

Brent Yorgey @byorgey@mathstodon.xyz · Apr 15, 2026

Replying to @wilbowma@types.pl

@wilbowma Alas, if only this actually meant anything. It would be hilarious if the next person who searches for something with Google gets an AI Overview with a bunch of 'damn's in it

2

0

Brent Yorgey @byorgey@mathstodon.xyz · Apr 09, 2026

Replying to @andrejbauer@mathstodon.xyz

@andrejbauer Pick a random multiset of rotations of the square, with cardinality five. Now stand in one spot, and perform every possible permutation of the rotations by rotating in place.

1

0

Brent Yorgey @byorgey@mathstodon.xyz · May 20, 2025

Replying to @mjd@mathstodon.xyz

@mjd Machine learning systems can already do that! ...oh, wait, you mean you also want their diagnoses to be accurate?

0

Brent Yorgey

Posts

Remote instance

Media