ProofWiki: Online compendium of mathematical proofs | Hacker News Reader

ProofWiki: Online compendium of mathematical proofs

proofwiki.org

154 pointsTomte32 comments

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!

I found a more detailed explanation of that proof at https://www.youtube.com/watch?v=4ApWBYBsc9k

It also wasn't immediately clear to me that this _is_ a valid sample space, the explanation in https://old.reddit.com/r/math/comments/18szn6y/anyone_use_pr... provides a more formal but still readable construction

I especially like the "finite" variant/version of the proof which reframes this as a counting/combinatorial proof instead of a probability-based one.

> However, we also see that for only those combinations starting with a T (that is f(n - 1))...

Why is that f(n - 1)?

The set of sequences of length n ending in HH (and with no earlier HH) and beginning with a T are in bijection with the set of sequences of length n-1 ending in HH (and with no earlier HH) by the bijection

   def f(s):
     assert(s[0] == 'T')
     return s[1:]

whose inverse is

  def f_inverse(s):
    return 'T' + s

Also the bijection between sequence of length n ending in HH (and no earlier HH) and beginning with an H are a bijection with the set of sequences of length n-2 ending in HH (with no earlier HH) by the bijection:

    def f(s):
        assert(s[0] == 'H')
        assert(s[1] == 'T')  # can't be another H!

    def f_inverse(s):
        return 'HT' + s

Therefore, since sequences either begin with a T or an H, for n>=2 we see f(n) = f(n-1) + f(n-2).

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

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.

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

> Verbal skills are apparently more predictive of programming career success than math scores.

This is an urban legend inspired by this article [1]. One problem with this research though is that it studies language learning. Not how good a programmer one becomes, and certainly not career success.

[1]: Relating Natural Language Aptitude to Individual Differences in Learning Programming Languages. https://www.nature.com/articles/s41598-020-60661-8

> Verbal skills are apparently more predictive of programming career success than math scores.

Curious about the references!

I've heard this and always thought it was probably true even setting aside the soft skills part of the job, but that was before data engineering and data scientists were common titles. If it ever was true, the situation is probably more nuanced now than it used to be

I guess it means they're not testing on logic in the math exam, or are verbal scores predictive of coding but not logic scores; maybe it's more of a G factor.

Not all lean proofs are actually computable, see the computable function link in the url you gave.

Not all code functions are mathematical functions. An expression can describe a relation that is not a function per the definition like "a function always returns one output for one input".

Function (mathematics) https://en.wikipedia.org/wiki/Function_(mathematics)

The Navier-Stokes equations are PDEs, not functions; but are they computable in Lean, or can algorithms for finding solutions be expressed in Lean?

Lean docs > Missing undergraduate mathematics in mathlib: https://leanprover-community.github.io/undergrad_todo.html#:...

Is ℯ^(2ί π x) a function? It's a complex function, but Geogebra draws it as a ~ (unit circle) + (y=0 if x > 0).

What I mean is lean can prove things like one of cantors theorems, the proof of which requires you to derive from properties on a function f showing that there exists a function g inverse to f, and show something about the results of calling g.

such a function in lean is considered non-computable by lean because it cannot be evaluated by lean since g has merely been shown to exist.

Many proofs in lean however are computable, just not all.

I don't think SymPy has abstract Function attributes to reason about, but it does have limited reasoning about number classes given e.g. `x = Symbol('x', real=True)`

SymPy docs > Writing Custom Functions > Easy Cases: Fully Symbolic or Fully Evaluated: https://docs.sympy.org/latest/guides/custom-functions.html#w...

If there is some sort of e.g. geometric correspondence, it could be possible for a Church-Turing classical computer to compute quantum functions (that return wave functions) that a Church-Turing-Deutsch quantum computer can compute; but otherwise Lean can't compute most quantum circuits either.

What I like most about ProofWiki is its sometimes nonstandard notations. For example, the interval notation: https://proofwiki.org/wiki/Definition:Real_Interval/Notation

The ads significantly impact credibility for a site like this IMHO.

Fortunately I don't see any ad

Indeed I was always very mystified when people complain about Youtube ads until Youtube started to mess with ad blockers. This made me consider stopping using Youtube altogether but fortunately uBlock Origin catched up.

Agree - and not simply the presence of ads, but the scammy, fraudulent type. I just saw the tiniest “X” to close an ad I’ve ever seen. And clicking it just opened the advertisers site anyway.

That’s not a sustainable strategy, that’s just fraud.

ProofWiki is an online compendium of mathematical proofs - https://news.ycombinator.com/item?id=31293073 - May 2022 (16 comments)

In https://proofwiki.org/wiki/Definition:Graham%27s_Number

it states "Amusingly, given that Graham's number is an upper bound, the actual solution to the problem in question, according to certain experts, may well be 6. "

I cannot edit the page but I believe they're up to at least 13 now.

"Stem Formulas" (2023) https://news.ycombinator.com/item?id=36817851#36839925

I remember findind this site when solving exercise of creating sign function for Z with arithmetic operators only. I used this[1] page to cheat and reimplement mod in C (by default % is rem) with defined zero. Unfortunately it doesn't helped me yet, but I still like this site.

[1]: https://proofwiki.org/wiki/Definition:Modulo_Operation/Modul...

The compendia of Metamath proofs us here https://us.metamath.org/

All of theree are formally from axioms or other formal proofs that lead back to their axioms, without any gaps.

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." :/

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.

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.

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.

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.

What is your certainty that that statement is true? What if it was a calculation which takes decades on a supercomputer?

At current rates, whatever is done on a supercomputer today is done by a cheap pocket-size device just decades later. So, I'm not too worried about this case.

One of the first famous examples of this is the four-coloring theorem. I don't know any serious mathematician who is not certain of that result.

Reply on news.ycombinator.com