Also have my resume and other such projects on the server
40 karma · joined May 14, 2025
Also have my resume and other such projects on the server
I wonder if there are some other related problems for small-n cases that I could add somewhere on this website?
Github repo for the site: https://github.com/tejstead/heilbronn-site
Also, check out the entry for square n=16, I added a pretty cool animation 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 ; QuantCoI 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.