Hacker News Reader

Comment by geysersam | Hacker News Reader

I think you're hitting the nail on the head here. Something about the learning process makes programming much easier to pick up.

What if we had something similar for mathematics?

Rapid feedback, error messages, maybe even linters and highlighting for the "mathematical syntax".

I've though about this before and I think tools like this could unlock math for a lot of people, and also increase the effectiveness of professional mathematicians.

When learning math / seeing other learning math I've noticed that simple errors such as typos often slow down or hinder understanding of the subject.

View on HN

Take a look at the Natural Number Game! [1] It does exactly that: "Rapid feedback, error messages, maybe even linters and highlighting for the "mathematical syntax"."

After you get the hang of the system, you can play with the interactive theorem prover behind it: Lean [2]. There's also plenty other interactive theorem provers (Coq, Isabelle, HOL, Mizar, Metamath, ...) but Lean has a lot of traction amongst mathematicians at the moment.

There are no limits to the math you an do with this. There is mathlib [3], the main mathematical library. It covers a lot of undergraduate material [4], and plenty of stuff beyond that [5]. The community has even covered some state of the art research math in Lean [6a, 6b].

You are very welcome to hang out on the leanprover zulip [7]] and ask questions about the Natural Number Game or anything else that is Lean-related.

[1]: https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_gam... [2]: https://leanprover-community.github.io/ [3]: https://github.com/leanprover-community/mathlib [4]: https://leanprover-community.github.io/undergrad.html [5]: https://leanprover-community.github.io/mathlib-overview.html [6a]: https://github.com/leanprover-community/lean-liquid [6b]: https://www.nature.com/articles/d41586-021-01627-2 [7]: https://leanprover.zulipchat.com/

Is it the learning process, or the subject itself?

Programming works with manmade abstractions, carefully designed to have very few interactions, keep mutable state contained, and to have all the parts structured in a hierarchy without recursion.

In math you have systems of equations that all reference each other. And they all happen at the same time because there's no steps and time or lines of code just 5 equations that all interact.

The atomic pieces are much larger and tied together and it inherently seems to require being able to fit nontrivial ideas in your head.

Programming lets you design a complex architecture one tiny piece at a time without considering other pieces.

Isn’t math just manmade abstractions as well? I’m not saying they’re equally hard (I think maths is harder too), but you seem to be overly simplifying programming, under the assumption that the system you are working with and building on is actually well designed, rather than what is actually more likely (a munge of SOME clean design with many layers of hacks on top).

I think Maths is harder because the abstractions are higher level, have less intuitive bases, the feedback loop is longer and doesn’t have robust testing. I don’t think the abstractions themselves are that much harder in general, but getting an intuition and doing anything useful (correctly) at a really high level of abstraction is quite difficult.

My view is that math is man made. It's a mash of notation for various ideas, more or less unambiguous, more or less rigorous. Some are more well designed than others. It's closer to natural language than programming languages.

Not every programming language has a concept of time. Sometimes that's a good thing, it depends on what you're used to. Math arguably has less mutable state than most typical programing languages.

I'd love to play around with such tools, but I think they'd only get you so far before they'd start to become a hinderance.

The linter in mathematics is whether the other mathematician (whoever you're proving to) knows what you mean. If you're locked into a rigidly defined syntax, an obvious line of questioning is: what's not expressible in this syntax?

I fear that by the time the tooling was agreed on, built, and taught in schools, you'd have something like APL, which might be cool to code in, but from which the mathematical conversion would have moved on a while ago. Efforts like that, after all, are how math becomes engineering.

Consider, for instance, Russel's theory of types, which was interesting math at the time and now strikes the student with an engineering background as "pretty much just Java" (or any "normal" statically typed language).

If you're learning math for career reasons rather than just pure curiosity, engineering is the main/possibly only place you'd use it besides statistical analysis.

Yeah that sounds about right. I was more musing about the philosophical boundary between math and engineering (math being a creative pursuit and engineering being about outcomes).

I can't quite pin it down, like with a definition, but I'm tempted to say that if it has a linter it's not math anymore, even if it once was.

I think this is the goal of proof assistants based on the Curry-Howard isomorphism, which the original author thought to denigrate for some reason.

What a creative, delightful solution. I encourage you to pursue this!

Reply on news.ycombinator.com