Hacker News Reader

Well, as a computer scientist, I'd urge them to reconsider. :) My intuition is that, given a sufficiently formalized system, computers can help them achieve their goal of understanding and discovering more math, much more rapidly and with compounding effects. Although perhaps there is a risk that any mathematics the computer might "discover" would become increasingly incomprehensible to human mathematicians, in which case the discoveries wouldn't be worth much.

I agree that humans are better at borrowing techniques between fields, but we can't do it quickly, and we can't systematically mine the entire "codebase" for these relationships (hence why "discoveries" in 2020 can combine ideas from 1990 and 2000). Besides, I suspect much of that gap between human and computer ability is due to a lack of a properly formalized representation of the ideas within each possibly related field. To use a programming term, it's a "code smell" if we haven't properly encoded the relationships between two fields. Sure, we can manually identify them, and then build on them once we do. But why did we need to bother in the first place? Wouldn't a formal system have made the relationships obvious, or at least more automatically discoverable?

Large language models have also changed my view of what computers are capable of, and in that context I've been most impressed with their ability to analogize and explain relationships between seemingly arbitrary sets of ideas. It makes sense they'd be good at this, since the premise of training them is to construct a web of weights that's indecipherable to humans but fundamentally enabling to the language model. Stephen Wolfram has been writing about how language models seem to encode a certain "truth" which has always existed but which we've never recognized. This idea resonates with me and I expect models have a lot to teach us about our own consciousness and how we model the world.

But on the other hand, if LLMs are so successful, by definition, at identifying relationships without being given formal representations of them, then why bother formalizing mathematics? After all, mathematics only exists because we can communicate its ideas by constructing the language of mathematics as a sort of amalgam of spoken language and abstractions we create within it. And while the exercise of formalizing the relationships between those abstractions might identify some imprecisions or mistaken assumptions in the existing hybrid of spoken language and formalized chunks of math, do we really need to bother? For an advanced LLM, shouldn't our existing definitions become naturally encoded into its weights during training, so that any emergent formalisms can be poked and prodded when we talk to it or ask it to reason about them? Or will it get stuck on the same imprecisions that we might identify when trying to manually formalize our existing systems of mathematics?

I don't quite understand what you are saying about llms. Language models are sort of a reverse engineering of the ways humans learn. I imagine if you read basically the whole internet and meaningfully memorized it you would be able to connect a bunch of dots too. Computers are just fast. Math viewed as tool doesn't require formalization, math as an endevour does. Sometimes exploring a theory is useful sometimes it's only interesting in itself

Asking working mathematicians to formalize their proofs in a machine-checkable system is like asking photographers to become electronics engineers so they can build their own digital cameras from scratch. It's not a reasonable request. It's so far outside of a typical mathematician's lane it's not even on the same continent.

They could do what every other scientist does, and pay people to build and run the tools they need to get scientifically valid results from their experiments.

Math isn’t science. Most mathematicians aren’t interested in applications to the real world. They don’t care about empiricism or validity. The fact that a lot of applications have come out of math is a side effect.

Imagine if someone discovered a way to solve real world problems by formulating them as chess positions. Would it be reasonable of us to demand that chess players stop competing and work on these formulations? No, and I don’t think many chess players would jump at the opportunity. They just want to play chess!

> Most mathematicians aren't interested in refactoring their mathematical "codebase", nor experimenting with axioms. They simply want to understand and discover more math.

Experimenting with axioms is one way you discover more math. For example, set theory: there’s a lot of math assuming ZF(C), but even more if you start looking at alternatives to it (like NBG, NF(U), constructive set theories, non-well-founded set theories, paraconsistent set theories, etc)

You're not wrong, but most mathematicians aren't working on (or even interested in) foundations. Not saying what you mentioned isn't math (I think it is), but my point still stands.

Very insightful. I can add famously, the parallel lines axiom of classical geometry that when changed created hyperbolic geometry.

I am a mathematician and would love to mechanize my proofs. The issue is that systems like Coq construct proofs in a radically different way than how we were trained. I've struggled with Coq even with a somewhat more than a passing knowledge of the system; I used Coq's underlying language Gallina to write interpreters, which were then processed into OCaml while studying in graduate school. At the same time, I can barely turn out a basic proof in Coq.

What would help dramatically for me and others that work in applied math are proofs that cover the material in something like Principles of Mathematical Analysis by Walter Rudin. These are proofs that cover basic real analysis and topics like continuity, differentiation, and integration. It would also help to see basic linear algebra proofs such as that all real symmetric matrices have a real eigendecomposition. Now, these may exist and it's been a couple of years since I've looked. If anyone has a link to them, I'd be extraordinary grateful.

For the math that you mention, I would suggest looking at mathlib (https://github.com/leanprover-community/mathlib). I agree that the foundations of Coq are somewhat distanced from the foundations most mathematicians are trained in. Lean/mathlib might be a bit more familiar, not sure. That said, I don't see any obstacles to developing classical real analysis or linear algebra in Coq, once you've gotten used to writing proofs in it.

I'm curious, which field of math do you work in?

Edit: for example, that symmetric matrices have real eigenvalues is shown here in mathlib: https://leanprover-community.github.io/mathlib_docs/analysis...

Thanks for sending by the mathlib examples. They're not particularly intelligible for me, but it's something to work towards.

Generally speaking, I work in the intersection between optimization, differential equations, and control. To that end, there's a variety of foundational results in things like optimization theory that I'd like to see formalized such as optimality conditions, convergence guarantees, and convergence rates.

Two questions if you know. One, which theorem prover would you recommend for working toward these kinds of results? Two, is there appetite or a place to publish older, known theorems that have been reworked and validated? And, to be clear, two is not particularly important for me and my career, but it is for many of my colleagues and I'm not sure what to tell them about it.

You're welcome! And likewise, thanks for the interesting reply.

I'm afraid I have no knowledge of your field, and no idea whether there are good tools and libraries for formalising the things you want. Maybe ask or have a look around the Proof Assistants StackExchange[1]?

There are many CS conferences through which you can publish formalised mathematics. One that comes to mind is ITP[2], but there are lots which are announced on mailing lists like TYPES-announce, coq-club, agda... You could look through previous versions of ITP and check out a few of the papers on formalising mathematics to get a feel for what these publications look like.

[1] https://proofassistants.stackexchange.com/

[2] https://mizar.uwb.edu.pl/ITP2023/

I am nothing more than an enthusiastic dabbler, but these have helped me.

There are two very different directions 1. the sort of full on proof automation with tactics https://direct.mit.edu/books/oa-monograph/4021/Certified-Pro... Dr. Chlipala builds up understanding of the "crush" tactic, which more or less lets you specify an inductive hypothesis, and that tactic fiddles around with identifying the base case, and expanding enough to generate the n+1 step. Along the way, you get exposure to using Gallina to write your own tactics.

it's neat, from a programmer point of view, because you can automate away the boring parts. There is pretty good discussion of debugging tactics, which might provide a path to transforming machine proofs into something a bit more comprehensible. at the very least, you can recover the application of axioms and such that did the transformation.

The other direction, that has been much more enlightening for me (the amateur hobbyist) was agda and Jesper Cockx's tutorial- https://github.com/jespercockx/agda-lecture-notes/blob/maste... he builds up all of the notation from, well, nothing. for example, you get refl, and then build up

  -- symmetry of equality
  sym : {A : Set} {x y : A} → x ≡ y → y ≡ x sym refl = refl
  -- transitivity of equality
  trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z (54) trans refl refl = refl
  -- congruence of equality
  cong : {A B : Set} {x y : A} → (f : A → B) → x ≡ y → f x ≡ f y cong f refl = refl

along with the syntax that comes with the agda std lib. agda is different, but you can still extract to Haskell (and allegedly javascript for node, but that was a little flakey for me and might go away in a future release). less useful for your goals, much more programming oriented - https://plfa.github.io is pretty good, and worth mentioning as a reference.

I'm slow on replies, but thanks for the references. I'll have a look.

Is the problem that human mathematicians have decided that classical logic + ZF(C) is the best framework for them–but it isn’t the best framework for computers?

Which raises an interesting philosophical question - do contemporary mathematicians mostly do things one way rather than another (i.e. classical logic instead of intuitionistic/paraconsistent/etc logic, ZF(C) set theory instead of alternative set theories or type theory or whatever, classical analysis instead of non-standard analysis, and so on) - because they’ve settled upon the inherently superior (easier, more productive) way of doing things - or is that just an accident of history? Could it be that in some alternative timeline or parallel universe out there, mathematics took some different forks in the road, and the mathematical mainstream ended up looking very different from how it does here?

I find these "fork in the road" questions endlessly fascinating, and that's exactly what I was getting at with my comment about the motivation for formalizing mathematics. And it doesn't just apply to math, but the whole "tech tree" of human history. How many seemingly arbitrary choices led us down a path that unknowingly diverged from some alternative future?

Last time I commented about this [0], I made some guy irrationally angry as he told me I sounded like I was 19 years old. And in an earlier comment [1], another guy took extreme offense to my questioning of the statement "with enough marbles, the discrete distribution behaves like a continuous distribution."

It seems there is some high priesthood of mathematics and physics that doesn't like when you ask these sorts of questions.

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

[1] https://news.ycombinator.com/item?id=35201603

> Last time I commented about this [0], I made some guy irrationally angry as he told me I sounded like I was 19 years old

If people make comments like that, flag them and email dang (hn@ycombinator.com) and he’ll do something about them

> It seems there is some high priesthood of mathematics and physics that doesn't like when you ask these sorts of questions

In my personal experience, most professional mathematicians and physicists are open to questioning the foundations of their discipline, and deal charitably with doubters (even those who are coming from a place of misunderstanding).

I suspect most of the “high priests” you speak of aren’t actually professionals at all, just Internet randoms who (at best) know only slightly more than you do, and who know very little about the norms of civil dialogue

I can't speak for kxyvr, but let me chime in as a mathematician who does formalise my theorems. There's no issue with representing various foundations (e.g. ZFC) on a computer -- for example, that's essentially what Lean/mathlib does, and it's working out great for them. A "problem" with ZFC, however, is that it's very low-level, meaning there's a large distance between the "informal" proofs which mathematicians carry out and communicate, and their corresponding formal proofs in ZFC. Accordingly, for a ZFC-based mathematician to start using proof assistants, they not only have to learn how to use a proof assistant, but also to translate (or expand/elaborate) their math into ZFC.

In other foundations, such as homotopy type theory (which is what the article is about), the distance between "informal" mathematical arguments and their formal counterparts is much shorter. This is why formalisation is widespread in the HoTT-community. Indeed, I believe Voevodsky worked on HoTT in order to have a foundation which was much closer to the mathematical practice in homotopy theory.