Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

The Mathematical Hacker (2012)

evanmiller.org

Post reply on HN
Print view View original

141–150 of 186 posts

Re: The Mathematical Hacker (2012)

#141

Post by __MatrixMan__ »

nickelpro wrote: post #98
nextos wrote: post #97

Earlier quoted context omitted.

I think your comparison is a bit unfair. Essentially, CS is as hard as mathematics because it is mathematics. For example, take any good static analyzer that implements abstract interpretation. It generally works using Galois connections, which is just abstract algebra. Dijkstra's algorithm or A* came pretty early in the history of CS. It would be fair to compare their difficulty to something similar in mathematics,…

CS may be mathematics but programming certainly isn't If you're discussing pure CS, the thing you can write down in a book and for which a computer is a largely theoretical device, sure CS is mathematics. If we're talking about the practical reality that CS majors in America today are trying to achieve, and their undergraduate programs are trying to prepare them for, that's becoming a working programmer and has very…

I wish we'd just start issuing software engineering degrees so it would be easier to get an actual computer science education.

Re: The Mathematical Hacker (2012)

#142

Post by [deleted] »

geysersam wrote: post #114
nickelpro wrote: post #69

Earlier quoted context omitted.

I would hard disagree that undergrad level Analysis or even just the trickier corners of vector calculus are within the bounds of what programmers can easily pick up without dedicated and guided study. Everybody's gangster until they have to parameterize some bullshit helical structure in R3. Comparable levels of programming, what we expect of CS juniors, are regularly picked up by "the guy who is good with Excel" in…

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 profes…

[deleted]

Re: The Mathematical Hacker (2012)

#143

Post by constantcrying »

kaashif wrote: post #126
constantcrying wrote: post #95

Earlier quoted context omitted.

>isomorphic Certainly not every computation is a proof. What statement does: void f(){ printf("?"); } prove?

The fact that you have found a function of type () -> () is a proof that true implies true. This is the Curry-Howard isomorphism. Not a particularly interesting proof.

But surely there are uncomputable objects which you can make mathematical statements about. How do you encode them into a type signature?

Re: The Mathematical Hacker (2012)

#144

Post by deadbeef57 »

geysersam wrote: post #114
nickelpro wrote: post #69

Earlier quoted context omitted.

I would hard disagree that undergrad level Analysis or even just the trickier corners of vector calculus are within the bounds of what programmers can easily pick up without dedicated and guided study. Everybody's gangster until they have to parameterize some bullshit helical structure in R3. Comparable levels of programming, what we expect of CS juniors, are regularly picked up by "the guy who is good with Excel" in…

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 profes…

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/

Re: The Mathematical Hacker (2012)

#145

Post by defrost »

constantcrying wrote: post #143
kaashif wrote: post #126

Earlier quoted context omitted.

The fact that you have found a function of type () -> () is a proof that true implies true. This is the Curry-Howard isomorphism. Not a particularly interesting proof.

But surely there are uncomputable objects which you can make mathematical statements about. How do you encode them into a type signature?

> But surely there are uncomputable objects which you can make mathematical statements about.

Absolutely, one famous example is the halting function that has type (program description, program input) returns boolean.

A symbolic formal system can "reason about reason" and manipulate descriptions of objects that are themselves uncomputable, countably infinte, or even uncountably infinite.

Re: The Mathematical Hacker (2012)

#146

Post by mathgladiator »

tombert wrote: post #22
bmitc wrote: post #9

In Steve Yegge’s linked post: > Math is a lot easier to pick up after you know how to program. In fact, if you're a halfway decent programmer, you'll find it's almost a snap. This couldn’t be more wrong. Mathematics is the hardest thing I have ever done. I’m sorry, but mathematics is orders of magnitude more intensive and difficult than most programming. A simple fact that shows this is the amount of programmers who…

I think Yegge is actually completely correct. I started to learn to program when I was 14, and once I understood the concept of functions, I found it much easier to do my calculus and physics work. Fundamentally I understood how to break things down into computable steps. Granted, I think get the impression we might be overloading the term "mathematics".

> get the impression we might be overloading the term "mathematics".

We are; the challenge is there is a near infinite difficulty in both "programming" and "mathematics" and at a certain point, the skill sets diverge greatly.

Re: The Mathematical Hacker (2012)

#147

Post by BeetleB »

kaashif wrote: post #125
BeetleB wrote: post #58

Earlier quoted context omitted.

For most mathematicians, calculus as is often taught in typical undergrads is not "true" mathematics. It's just a tool for computation. For them, calculus is analysis (theorems/proofs that are used to build up calculus). So my question is: Did you study analysis and would you credit programming in helping you get good at it?

I don't understand this comment. Calculus as taught to mathematics undergrads is analysis, right? Where is calculus "often taught" without "theorems/proofs that are used to build up calculus"?

In most US universities, the courses called "calculus" are mostly about computing integrals and derivatives. Yes, they'll have some theorems (Fundamental Theorem, Mean Value Theorem, etc), but most of the problems are related to computation than proving.

Unfortunately, since engineering students outnumber math majors by a large margin, the departments cater to them and not the math majors. The latter study analysis in later years - usually third or fourth.[1] Universities with strong math programs may offer it in the first or second year.

[1] I just checked my undergrad's program. They begin taking analysis in their 4th year, and it's offered only one semester a year!

Re: The Mathematical Hacker (2012)

#148

Post by defrost »

BeetleB wrote: post #147
kaashif wrote: post #125

Earlier quoted context omitted.

I don't understand this comment. Calculus as taught to mathematics undergrads is analysis, right? Where is calculus "often taught" without "theorems/proofs that are used to build up calculus"?

In most US universities, the courses called "calculus" are mostly about computing integrals and derivatives. Yes, they'll have some theorems (Fundamental Theorem, Mean Value Theorem, etc), but most of the problems are related to computation than proving. Unfortunately, since engineering students outnumber math majors by a large margin, the departments cater to them and not the math majors. The latter study analysis i…

That's just sad.

I was taught Calculus in high school, years 11 and 12 (two optional senior years for those that want more education prior to university, etc rather than transfer to a trade apprenticeship or leave school altogether).

That was a mixture of basic theory and proof and some computation (eg: derive an expression for the volume of intersection of two pipes at right angles, etc).

University went straight in to heavy analysis and foundations (for Math 100 - math for the serious (math, physics, hard chemistry)), with seperate streams for "casual math" - engineering, business, law, etc.

Engineering math prepped people for calculating dynamics and kinetics with vary loads, masses, thrusts, harmonic forces, network propagation, mesh computations, etc.

This was Australia in 1980.

Re: The Mathematical Hacker (2012)

#149

Post by bibanez »

mschoenert wrote: post #82
zozbot234 wrote: post #26

Earlier quoted context omitted.

The matrix based method for Fib can be understood as applying the closed-form solution over Q(sqrt5). OP seems to miss this point.

My thoughts at this point in the original article was: Well - if you want to demonstrate how mathematics helps here, then you should mention that computing the n-th fibonnaci number can be computed as the n-th power of the matrix [[1,0],[1,1]], and that the most efficient way to compute powers (in any associative domain) is the repeated squaring algorithm.

There are many ways to obtain the formula mentioned in the article. One of them is by diagonalizing this matrix and then applying exponentiation. How can another algorithm be better than constant time in the most general case?

Re: The Mathematical Hacker (2012)

#150

Post by hnews_account_1 »

constantcrying wrote: post #52
edgyquant wrote: post #37

Earlier quoted context omitted.

I disagree because Math is programming. All those symbols you see map to a set of steps (a program.). It’s just knowing what subroutine every esoteric symbol stands for that’s hard. I will agree it’s been more difficult learning math than programming for myself as well: but that’s because math is geared and targeted for people who like doing symbolic logic by hand. Math people think we’re a level below them (we are i…

>All those symbols you see map to a set of steps (a program.) Simply not true. Most mathematical statements, e.g. proofs of existence have no relation to a "program". >math is geared and targeted for people who like doing symbolic logic by hand. No, it is not. There is absolutely nothing interesting about symbol manipulation, it is always the least interesting part of a proof. It usually is the part the author handwa…

The first part of your answer is incorrect about programming in a general sense (not the particular software programming most of HN does). I push it so far back as to call it programming in a computer science sense, which is very simply just proof theory encoded into a system.

There is a reason Turing is considered one of the greatest minds to ever live. He didn’t just invent a concept. He invented a completely new branch of science. We would’ve gotten there eventually but his idea to solve the Entscheidungsproblem using his machine was such a step ahead of the times that we christened him the father of an entire science.

Post reply on HN