Why Formalize Mathematics – More Than Catching Errors
Posted3 months agoActive3 months ago
rkirov.github.ioResearchstory
calmpositive
Debate
0/100
Formal VerificationMathematicsLean
Key topics
Formal Verification
Mathematics
Lean
The article discusses the benefits of formalizing mathematics using tools like Lean, going beyond just error checking, and the HN community shows interest in the topic.
Snapshot generated from the HN discussion
Discussion Activity
Light discussionFirst comment
47m
Peak period
1
0-1h
Avg / period
1
Key moments
- 01Story posted
Oct 18, 2025 at 3:01 AM EDT
3 months ago
Step 01 - 02First comment
Oct 18, 2025 at 3:49 AM EDT
47m after posting
Step 02 - 03Peak activity
1 comments in 0-1h
Hottest window of the conversation
Step 03 - 04Latest activity
Oct 18, 2025 at 3:49 AM EDT
3 months ago
Step 04
Generating AI Summary...
Analyzing up to 500 comments to identify key contributors and discussion patterns
ID: 45625479Type: storyLast synced: 11/17/2025, 9:03:50 AM
Want the full context?
Jump to the original sources
Read the primary article or dive into the live Hacker News thread when you're ready.
For TS I really just need some solid notion about sets, maybe some experience with generics, and patience to deal with how other people annotated their types if I want to use their code. It's not that big of a deal.
Math on the other hand, has lots of stuff formalized. Personally, doesn't feel like I can just jump in into one of those formal systems and thrive. It's way more than sets.
Perhaps the post is not for me. It's for people above me in math skills. In fact, I'm sure of it! But maybe there's some curious people that know TS and could be led to believe formal math is also just annotating types and doing sets, when I know that it's not! Analogies can be tricky sometimes.