987654321 / 123456789

The other replies are good, but let's add another one anyway.

0.987654321/0.123456789 = (1.11111111-x)/x = 1.11111111/x - 1 where x = 0.123456789

You can aproxímate 1.11111111 by 10/9 and aproxímate x = 0.123456789 using y = 0.123456789ABCD... = 0.123456789(10)(11)(12)(13)... that is a number in base 10 that is not written correctly and has digits that are greater than 9. I.E. y = sum_i>0 i/10^i

Now you can consider the function f(t) = t + 2 t^2 + 3 t^3 + 4 t^4 + ... = sum_i>0 i*t^i and y is just y=f(0.1).

And also consider an auxiliary function g(t) = t + t^2 + t^3 + t^4 + ... = sum_i>0 1*t^i . A nice property is that g(t)= 1/(1-t) when -1The problem with g is that it lacks the coefficients, but that can be solved taking the derivative. g'(t) = 1 + 2 t + 3 t^2 + 4 t^3 + ... Now the coefficients are shifted but it can be solved multiplying by t. So f(t)=t*g'(t).

So f(t) = t * (1/(1-t))' = t * (1/(1-t)^2) = t/(1-t)^2

and y = f(0.1) = .1/.9^2 = 10/81

then 0.987654321/0.123456789 ~= (10/9-y)/y = 10/(9y)-1 = 9 - 1 = 8

Now add some error bounds using the Taylor method to get the difference between x and y, and also a bound for the difference between 1.11111111 an 10/9. It shoud take like 15 minutes to get all the details right, but I'm too lazy.

(As I said in another comment, all these series have a good convergence for |z|<1, so by standards methods of complex analysis all the series tricks are correct.)

The even simpler example is more striking imo.

(147 + 369) / 2 = 258

and

(741 + 963) / 2 = 852

Well, in theory (and I guess more generally philosophy) land, sure, you can't really "prove absoluteness" outside of your axioms and assumptions. You need to have a notion of true and false, and then implications, for example, to do logic, then whatever the leap from there it takes to do set theory, then go up from there etc. it's turtles all the way down.

In practice land (real theorem provers), I guess the idea is that, it theoretically should be a perfect logic engine. Two issues:

1. What if there's a compiler bug?

2. How do I "know" that I actually compiled "what I meant" to this logic engine?

(which are re-statements of what I said in theory land). You are given, that supposedly, within your internal logic engine, you have a proof, and you want to translate it to a "universal" one.

I guess the idea is, in practice, you just hope that slight perturbations to either your mental model, the translation, or even the compiler itself, just "hard fail". Just hope it's a very not-continuous space and violating boundaries fail the self-consistency check.

(As opposed to, for example, physical engineering, which generally doesn't allow hard failure and has a bunch of controls and guards in mind, and it's very much a continuuum).

A trivial example is how easy it is to just typo a constant or a variable name in a normal programming language, and the program still compiles fine (this is why we have tests!). The idea is, that, down from trivial errors like that, all the way up to fundamental misconceptions and such, you can catch preturbations to the ideal, I guess, be they small or large. I think what makes one of these theorem provers minimally good, is that you can't easily, accidentally encode a concept wrong (from high level model A to low level theorem proving model B), for a variety of reasons. Then of course, runtime efficiency, ergonomics etc. come later.

Of course, this brings into notion just how "powerful" certain models bring - my friend is doing a research project with these, something as simple as "proving a dfs works to solve a problem" is apparently horrible.

this reminds me of the online encyclopedia of integer sequences (https://oeis.org/). anything similar for things like 987654321 / 123456789 ?