Tetration?

Stream: new members

[Arndt Schnabel]

Just saw this video: https://www.youtube.com/watch?v=BdHFLfv-ThQ

How would this statement look like in Lean?

[Riccardo Brasca]

Stating this seems easy.

import analysis.special_functions.pow

open_locale real

open real

example : ∃ (n : ℕ), π ^ π ^ π ^ π = n := sorry

[Arndt Schnabel]

Is it also possible to state the general case, pi raised to itself an arbitrary number of times?

Something like

example : ∃ (x, n : ℕ), π ^^ x = n := sorry

[Eric Wieser]

You can use something like function.iterate (^ π)

[Riccardo Brasca]

Well, essentially all math results can be stated, and in principle proved, in Lean. Sometimes it is difficult, but I don't see any problem here.

[Riccardo Brasca]

Arndt Schnabel said:

Is it also possible to state the general case, pi raised to itself an arbitrary number of times?

Something like

example : ∃ (x, n : ℕ), π ^^ x = n := sorry

I can even prove this statement :D Can you find your error?

[Arndt Schnabel]

Yep ^^, missed the x=0 case :) (Is there an ℕ+ or would it be better to add a x > 0 constraint?)

[Riccardo Brasca]

The point is that you want this for all x.

[Riccardo Brasca]

In mathlib I don't think we have a definition of tetration, but as Eric said, this not a problem.

[Eric Wieser]

The definition would look something like this:

def tetrate {R} [has_one R] [has_pow R R] (r : R) : ℕ → R
| 0 := 1
| (n + 1) := r ^ tetrate n

infix ` ^^ `:80 := tetrate

[Arndt Schnabel]

Does mathlib contain yet unproven problems like these (so we could perhaps give them to automated theorem provers and see what they do with it? I wonder what the cutting edge solvers' 'expected provability' of this statement is :thinking:)

[Riccardo Brasca]

mathlib does not contain unproved statements (there is a discussion on having a conjecture folder or something similar). In any case I am pretty sure we are years away from having an automatic solver proving a real conjecture.

[Reid Barton]

I doubt that any "cutting edge solver" knows the definition of π.

[Patrick Massot]

Riccardo, you should be more careful with your "real conjecture" terminology. Some people claim this already happened. A safer terminology is "a conjecture that I find relevant in an area of mathematics that I work in".

[Patrick Massot]

A classical example is https://en.wikipedia.org/wiki/Robbins_algebra.

[Patrick Johnson]

A more general hyperoperator function:

def hyper : ℕ → ℕ → ℕ → ℕ
| 0 a b := a + b
| 1 a b := a * b
| (n+2) a 0 := 1
| (n+2) a (b+1) := hyper (n + 1) a (hyper (n+2) a b)

Addition is hyper 0, multiplication is hyper 1, power is hyper 2, tetration is hyper 3, and so on.

[Patrick Johnson]

Can easily be extended to real numbers of course.

[Riccardo Brasca]

Yeah, I am maybe too pessimistic. I mean conjectures that require quite a lot of work to state. For example this one requires of course the definition of real numbers, the definition of π, of has_pow ℝ ℝ and so on. But I would be very happy to be proved wrong!!

[Mario Carneiro]

I would give automatic theorem provers a probability of approximately 0 to prove that pi^pi^pi^pi is or is not an integer

[Mario Carneiro]

that is not something you can "intelligent brute force" your way to a solution

[Arndt Schnabel]

It would be satisfying to see the progression from 0.000000000000001 to 0.0000000001 to 0.0001 over the years :)
Does anyone know any prover who actually gives such a value, predicting whether it can solve a problem in advance?

[Patrick Massot]

Note that I was commenting Riccardo's very general claim, not that specific problem.

[Mario Carneiro]

well, if there are ways to make the problem easier you can look at the success rate on such easier versions

[Mario Carneiro]

The only way you can make that problem easier that would make the success rate noticeably nonzero would be to make the numbers less astronomical so that you can actually bound the value

[Mario Carneiro]

anything else hits up against some hard number theory questions that are completely unsolved outside of theorems like Lindemann-Weierstrass

[Mario Carneiro]

and ATPs are no good at making much progress in this kind of pure mathematics so far

[Violeta Hernández]

What do you mean? It's just a matter of calculating the first or maybe the second decimal digit :P

[Violeta Hernández]

It would be conceptually easy, although computationally infeasible, to prove π ^^ 4 isn't an integer, assuming that it isn't

[Violeta Hernández]

Now if it turns out to be true by some sort of miracle, I give it a probability of 0 for a computer to prove this

[Mario Carneiro]

I didn't check the exact order of magnitude but I believe that this kind of example is designed specifically so that the number of digits you need is more than any computer could possibly work out

[Mario Carneiro]

looks like it's about $10^{6.6\times 10^{17}}$

[Mario Carneiro]

or $2^{2^{60.9}}$

[Mario Carneiro]

which is on the edge of what's humanly possible

[Mario Carneiro]

This requires an estimate of pi which is at least as precise, which is quite a bit beyond the best computation done so far: the recent computation of $10^{14}=2^{46.5}$ digits of pi is still only 76% of the way there, although since the algorithm is log-linear I think storage and parallel computation is the major bottleneck

[Violeta Hernández]

Wait, does this mean that computing trillions of digits of π might actually have some mathematical use?

[Violeta Hernández]

A really dumb use, but still