Cool work.

I wonder if contemporary proof assistants have enough primitives to implement this.

> pure math (topology and countability) and computer science have almost no overlap in the short term.

This is an unexpected opinion. What do you mean by this?

I would argue the opposite.

Look at Formal Verification[0].

Here's a great video about a popular formal verfication proof assitant: https://www.youtube.com/watch?v=Dp-mQ3HxgDE

A quote from the mathematician in the video expressing enthusiasm for using computers for mathematics: "All I want to do... I don't want to do mathematics on pen and paper anymore, because I don't trust it, and I don't trust other people that use it; which is everyone." (in case people only read this quote, instead of watching the lecture, the tone is tongue-in-cheek)

Formal Verification would seem a literal intersection of pure math (formal proofs[1]) and computer science (formal specification[2]).

Of note, one of the popular underlying foundations of an approach to formal verification is Homotopy Type Theory(HoTT)[3][4] which is an asserted effort to show the relationship between type theory and, specifically, topology (homotopy[5]).

[0] https://en.wikipedia.org/wiki/Formal_verification : fancy word for 'computer verified mathematical proofs'

[1] https://en.wikipedia.org/wiki/Formal_proof : fancy word for 'proof'

[2] https://en.wikipedia.org/wiki/Formal_specification : fancy word for 'rules for an algo that checks a proof'

[3] https://en.wikipedia.org/wiki/Homotopy_type_theory

[4] https://homotopytypetheory.org/book/ : a great read, even if you are a novice, or prefer other formal verification foundations

[5] https://en.wikipedia.org/wiki/Homotopy_theory : "It originated as a topic in algebraic topology"

I wonder(worry) that this dump is actually a key honeypot.

May have people thinking: "I already have a <STREAM-SERVICE> account, but with this I could at least get 4k."

They put their legitimate key in, and maybe it phones home the key before begining the download?

This comment from a previous thread illuminates some concerning oversights concerning public repository etiquette:

> I also noticed it provides part of the functionality with a .pyc file, without including the normal python source.[0]

[0] https://news.ycombinator.com/item?id=29704610