[HN Gopher] ProofWiki: Online compendium of mathematical proofs
___________________________________________________________________
ProofWiki: Online compendium of mathematical proofs
Author : Tomte
Score : 71 points
Date : 2024-02-04 17:51 UTC (5 hours ago)
(HTM) web link (proofwiki.org)
(TXT) w3m dump (proofwiki.org)
| gdsimoes wrote:
| What I like most about ProofWiki is its sometimes nonstandard
| notations. For example, the interval notation:
| https://proofwiki.org/wiki/Definition:Real_Interval/Notation
| dang wrote:
| Related:
|
| _ProofWiki is an online compendium of mathematical proofs_ -
| https://news.ycombinator.com/item?id=31293073 - May 2022 (16
| comments)
| alexmolas wrote:
| The featured proof about the sum of Fibonacci numbers divided by
| 2^n is beautiful.
|
| When I started reading the proof I thought it was a mistake, a
| mismatch between the theorem to proof and the linked proof. I
| didn't expect using Kolmogorov axioms to prove this kind of sums.
| I really enjoyed reading it. I just learned something new today,
| thanks!
| ivancho wrote:
| Their "proof" that there are only 12 solutions to 8 Mutually Non-
| Attacking Queens on Chessboard is just "That there are only these
| 12 can be proved by brute force." :/
| jusuhi wrote:
| The task proving some statement and the task of finding the
| shortest, or a "reasonably short" proof, are very different
| endeavours.
|
| The first is about certainty that a statement is valid
| ("true"). The other is about simplifying the understanding of
| _why_ it is valid. Most of the time, you don't care much about
| the latter.
| zamadatix wrote:
| It would be nice to have an reproducible example of how the
| result was achieved though. Otherwise it's a compendium of
| results, not proofs.
| ivancho wrote:
| What is your certainty that that statement is true? What if
| it was a calculation which takes decades on a supercomputer?
| geor9e wrote:
| You have proof in sarcasm quotes, but it counts
| https://en.wikipedia.org/wiki/Proof_by_exhaustion
|
| In my university math departments putnam problem competition
| (they'd just be on the wall, prize was a $40 giant pizza each
| week) they would accept the most elegant solution, so if nobody
| else submitted something better I'd get a pizza for just
| running a few lines of python.
| ivancho wrote:
| I'm not gatekeeping proofs here, and I'm glad you got math
| pizza :) If proofwiki had exhaustively printed all possible
| arrangements, or the decision tree of constructing them, or
| if they had even included the code that would do the checking
| (like, say, https://www.richard-
| towers.com/2023/03/11/typescripting-the-...), then I would
| agree it counts. But without even a rough ballpark estimate
| of possible arrangements to check, asserting "brute force"
| does not make a proof. If I incorporate understanding of the
| problem, I can see that at most we need to check 8!, which is
| reasonable. But if the constraints were not so simple, then
| we might be dealing with 64-choose-8 cases instead, which is
| heading into not-reasonable.
|
| They can add the same sentence under every finite fact in
| their wiki, but then it won't be a proof wiki, it would be a
| list of numeric facts they checked by brute force and we can
| either trust them, or check ourselves.
| westurner wrote:
| From "Ask HN: Did studying proof based math topics make you a
| better programmer?" https://news.ycombinator.com/item?id=36463580
| :
|
| > _Lean mathlib was originally a type checker proof assistant,
| but now leanprover-community is implementing like all math as
| proofs in Lean in the mathlib project_
|
| Lean Mathlib is composed of _executable_ proofs written in Lean:
| https://leanprover-community.github.io/mathlib-overview.html
| eduhetxub wrote:
| Be careful. While a proof in Lean is executable (it is a
| script, so to speak) it is conceptually a sequence of
| references to tactics. Writing a Lean proof does involve a
| highly specialised form of functional programming, but I
| wouldn't be at all sure that becoming an expert in Lean would
| improve your programming skills across the board.
|
| Your comment also reminds me of the people who claim that the
| Curry-Howard isomorphism means "programming is math". It's not
| a claim that anyone should really be making in good faith.
| There's a lot more to programming than the lambda calculus.
| westurner wrote:
| Verbal skills are apparently more predictive of programming
| career success than math scores.
|
| Is Quantum Logic the correct propositional logic? Is Quantum
| Logic a sufficient logic for all things?
|
| I'd much rather work with machine-checkable proofs; though
| Lean is not what I've been taught math in either.
|
| Coq-HoTT is written in Coq, not Lean.
|
| A tool that finds the correspondence between proofs as
| presented and checkable proofs in a reasonable syntax would
| be helpful, I think.
|
| If I start with "Why is 2+2=4?" [in this finite ring], I'm
| not sure how to find the relevant Lean code in Mathlib to
| prove my bias inductively, deductively, or abductively
| ratmice wrote:
| Not all lean proofs are actually computable, see the computable
| function link in the url you gave.
| photonthug wrote:
| The ads significantly impact credibility for a site like this
| IMHO.
___________________________________________________________________
(page generated 2024-02-04 23:00 UTC)