interesting how API and abstraction works in Lean. it's similar to programming but a slightly different feel to it. i'm replacing an abbrev (which is kind of like a transparent alias) with a def (more opaque) + small lemma for that def. notice how this simplifies code [github.com/gaearon/anal...](

GitHub

Section 3.6 solutions by gaearon · Pull Request #9 · gaearon/analysis-solutions

My solutions to Tao's Analysis I, formalized in Lean - Section 3.6 solutions by gaearon · Pull Request #9 · gaearon/analysis-solutions

)

seems like not sending this is severely hurting third party feeds ability to be even remotely competitive with Discover RE:

Bluesky Social

spacecowboy (@spacecowboy17.bsky.social)

Please let me know if you have any other suggestions. It would be great to receive "app.bsky.feed.defs#interactionSeen".

congruence is a cool word

notable: bsky is looking for machine learning engineers help bluesky fix Discover! RE:

Bluesky Social

hailey (@hailey.at)

more jobs more jobs. come apply!! bsky.social/about/join https://bsky.social/about/join

View quoted note →

why is X isomorphic to Unit → X but not to X → Unit? is there a good intuition for why putting X in the input position breaks isomorphism

which of these functions is cooler? y = 2^x y = e^x natural growth seems like a good argument for e^x but then 2^x describes the powerset...

i wonder if there's been some kind of a recent regression in the Discover codebase. my feed has a lot more "ntpc" segments now and they're all the stuff i don't want to see. how is this possibly related to my interests? why is Discover shoving these bad posts into my timeline https://morel.us-east.host.bsky.network/xrpc/com.atproto.sync.getBlob?did=did:plc:fpruhuo22xkm5o7ttr2ktxdo&cid=bafkreibhnzdyk6liyx64nc3eskbk4iamy4o3cfsx2dtgehnv2dbhh6z4dy https://morel.us-east.host.bsky.network/xrpc/com.atproto.sync.getBlob?did=did:plc:fpruhuo22xkm5o7ttr2ktxdo&cid=bafkreiaaxl7le55pchww5n4twxlanoupmnt2woc4lfgggzltdda2nzgf5q https://morel.us-east.host.bsky.network/xrpc/com.atproto.sync.getBlob?did=did:plc:fpruhuo22xkm5o7ttr2ktxdo&cid=bafkreif6nxytnabcm6im2ki2fd4wjkpgkngb2xux6q3lqorf3w45urmok4 https://morel.us-east.host.bsky.network/xrpc/com.atproto.sync.getBlob?did=did:plc:fpruhuo22xkm5o7ttr2ktxdo&cid=bafkreifktfkuosj3vsx5hhjxgllbnaq5wqqkp2jt3vlupwuk3wzqlqdg5e

[@spacecowboy17.bsky.social](

Bluesky Social

spacecowboy (@spacecowboy17.bsky.social)

Interests in ML and social aspects of tech. Building For You feed: https://bsky.app/profile/spacecowboy17.bsky.social/feed/for-you Hobby project:...

) do you have any plans for a "refreshable" For You? i'd like to use it as the main feed but i need the refresh to show new posts (and hide posts i've already seen)

the thing i hate about the Discover algorithm (well, one of those) is that its `popfriends` segment (which is great in theory) has no differentiation between "friends whose likes i appreciate" and "friends whose likes i never want to see". here's some of the latter: banal truisms repeated ad nauseam https://morel.us-east.host.bsky.network/xrpc/com.atproto.sync.getBlob?did=did:plc:fpruhuo22xkm5o7ttr2ktxdo&cid=bafkreifzmus2pkald5flp4pdelmcovp623hzvv6i7ozqmuc4n6rdrjeyda

doodling https://morel.us-east.host.bsky.network/xrpc/com.atproto.sync.getBlob?did=did:plc:fpruhuo22xkm5o7ttr2ktxdo&cid=bafkreicuwv3wbuzusfi2etgikuhemlahqozt3da4ywc5kwp3muaxpo4yvi