Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

In higher math (typically 2nd year and onwards at US universities) there is fairly little explicit calculation, and math is more about studying the (formal) relationships between mathematical objects. For example, we can abstractly define topological spaces and abstractly define algebraic “groups,” and algebraic topology studies the relationships between topological spaces and algebraic groups. This is somewhat like having a “data type” defined by some library, examining ways it can be transformed into data types defined by some other library, and studying what invariants hold under those transformations.

In some sense, an undergraduate math education is akin to learning the “standard library” (in the software engineering sense) of higher mathematics. Most courses start with basic abstractions of some mathematical object and repeatedly construct more and more abstractions on top of those. The structure of those abstractions is similar to how you might build a library. A professional mathematician is expected to be fluent in the mathematical standard library, just like how you might expect an experienced software engineer to be fluent in Python’s standard library.

If this analogy is true, people who can learn Python relatively quickly might be able to also learn higher mathematics relatively quickly under the right pedagogical environment.



One personal project I'd love to find the time for is to try to write out a sequence of math notes that essentially builds up a Lean repository, intentionally "refactoring" as it goes along. So you do some explicit coordinate vector or system-of-equation calculations with both real and complex numbers, eventually define interfaces for fields and vectors, do your linear algebra proofs, realize that linear endomorphisms are almost-but-not-quite a field, so define rings and go back and refactor your field proofs to use them, realize vector spaces are "K[T] not-quite vector spaces", define modules, refactor your vector space code, etc.

This was kind of how math classes worked, but without that explicit phrasing. It would certainly make the analogy between the two activities more obvious. I also wonder whether people would have less trouble with quantifiers if they were phrased in programming terms: a proof of "forall x, p(x)" is a function x=>p(x), and a proof of "there exists x such that p(x)" is a pair (x, p(x)). e.g.

Continuity: (epsilon: R, h: epsilon>0, x_0: R) => (delta: R, h2: (x: R, h3: d(x,x_0) < delta) => d(f(x),f(x_0)) < epsilon)

Uniform continuity: (epsilon: R, h: epsilon>0) => (delta: R, h2: (x: R, x_0: R, h3: d(x,x_0) < delta => d(f(x),f(x_0)) < epsilon))

proof of UC => C = (epsilon, h, x_0) => let delta, h2 = UC(epsilon,h) in (delta, h2(_,x_0,_))

So when you're trying to figure out how to do the proof, it's clear what kind of type you need to return and your IDE could help you with autocomplete based on type inference.




Consider applying for YC's Fall 2026 batch! Applications are open till July 27.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: