Hacker News Reader

vibecodermcswagon Lean 4 formalization of Erdős Problem #848 – seeking review

Formalized the Sawhney-Sellke stability theorem for Erdős Problem #848 (squarefree products) in Lean 4.

~3800 lines, compiles with 0 errors, no sorries, no axioms.

The math was solved by Sawhney & Sellke (Nov 2025): https://arxiv.org/abs/2511.16072

Only ~17 Erdős problems have full solutions formalized in Lean. If valid, this would be ~#18.

Done with multiple AI tools (Claude Opus 4.5, GPT-5.2, Gemini 3.0, Aristotle) + human orchestration.

Seeking review: Does this actually prove what it claims? The code is verbose and could be cleaner. Would appreciate expert eyes.

vibecodermcswagon Beyond sensor data: Foundation models of behavioral data from wearables

i love this because I build in medtech, but the big problem is no open weights, nor open data.

you can export your own apple XML data for usage and processing, but if you want to create an application and request apple XML data from users, that likely crosses into clinical research territory with data security policy requirements and de-identification needs.