Lattice Triangles Are Rare

axiommath.ai

29 points·skogstokig··4 comments

https://github.com/AxiomMath/lattice-triangle

It should be noted that this is a PR piece for a "math" startup. The result doesn't look particularly interesting, from either a mathematical or Lean code standpoint, as far as I can see.

Not sure about the significance of the result here, but this article just gave me the inspiration I needed to solve Project Euler #202: https://projecteuler.net/problem=202

Curious if the authors are hanging around here and how they feel about the recent Leiden Statement. (Late in the article it’s clear that this is at least partially a publicity effort around a new AI math tool, if I’m reading it correctly.)

On a personal level I’m very excited about AI getting good at math, but I’m a consumer of math, not a creator. My job gets easier as AI gets better on this front, so I can’t fully empathize with mathematicians who feel threatened or are worried about the sanctity of the discipline.

I am a producer of math. But I feel two ways about AI math.

First I fear slop-math. People producing LLM “proofs” and prose with no value. I do not want to review something the author has spend lies energy on than I will spend reviewing.

Two, I am excited about formal machine-checked proofs. I love formalisation, and if the llm can prove my lemmas I will be a happy camper!

I think my optimism here is coloured by the fact that I am a theory builder, not a problem solver. I will be happy to create beautiful theory, writing (myself) wonderful articles explaining them, but letting the ugly details be formally verified by an LLM.

A problem solver kind of mathematician might feel cheated of all the fun of the llm did all the problem solving.

Reply on news.ycombinator.com