tejstead

I think this is basically a copy of Gerrymandle?

I host https://math.tejstead.com - a little website about math.

Also have my resume and other such projects on the server

what?

If you want to make a PR to put in a new submission, feel free to do so. There's no particular reason why the site currently stops at 35-36 points, other than computational limits.

> This problem is related to a more general family of incidence geometry problems called 'lower bounds for incidences': given some collection of geometric objects (say, points and lines), under what conditions can we guarantee that there are in fact more 'almost incidences' than we originally expect?

I wonder if there are some other related problems for small-n cases that I could add somewhere on this website?

It seems like this post got put into some kind of "second chance" queue - thanks @dang! I'm around to answer questions if anyone has them.

Github repo for the site: https://github.com/tejstead/heilbronn-site

Hi there,

I made this website to showcase the Heilbronn problem, which is a classic problem in optimization. Lately there has been a wave of contributions of new records made by amateur mathematicians - you could be one of them!

  Location: Munich, Germany
  Remote: Open to it. Authorized to work in USA, Germany, UK, and Ireland.
  Willing to relocate: No; occasional travel is ok though
  Technologies: Python, Java, Terraform, Kubernetes, AWS, Azure, GCP
  Résumé/CV: https://tejstead.com/resume
  Email: chatgptej+hn [at] gmail.com

Experienced backend software engineer / platform engineer / SRE with an interest in reliability and cybersecurity. Ex-AWS ; QuantCo

I think this is why Terence Tao created https://palomar-registry.org (I have no affiliation with them besides also having sent in a result there)

> I am at a loss about what to do with these results.

I would recommend publishing them to Palomar (https://palomar-registry.org/) - I have no affiliation, this is an online registry of Lean-verified proofs created by Terrence Tao.

I have submitted a proof there that's also minorly important in an extremely niche field.

Anyway, I feel like it's a good place to dump AI slop lean proofs because the main point of the registry is that it verifies that: 1) your Lean challenge statement is the same as what you informally state you're trying to prove; 2) your Lean proof actually compiles.

This could be useful to future AI slop researchers who want to know if a given result has already been formalized, and they may be able to mine some lemmas from your work. Also, it's good to know for the field in general what has been proven.

I'm fairly certain you can set your publishing name to be whatever you want, so you could set it to be just the word "Anonymous", or the name of the model you used.