text:
Zero-sum counting
Write a program or function that given n ≥ 1 returns the number of solutions to ±1 ± 2 ± 3 ± ... ± n = 0.
For n = 6 there are no solutions, so the answer is 0. For n = 4 there are two solutions, so the answer is 2 (the two solutions are 1 - 2 - 3 + 4 = -1 + 2 + 3 - 4 = 0).
This is OEIS sequence A063865. Some example input/outpus are:
n       a(n)
1       0
2       0
3       2
4       2
5       0
6       0
7       8
8       14
9       0
10      0
11      70
12      124
13      0
14      0
15      722
16      1314

Shortest code in bytes wins.

Related

@ManishKundu Hm, I'd say that looks pretty much like a possible dupe target to me, just tack "length" at the end or instead of "filter by sum equals" do "sum each then count" to make an answer for this.

@EriktheOutgolfer I wasn't aware of that challenge, but the answer to this can be substantially different, see mine for example.

@ManishKundu I just explained how this challenge is different...

Welp, I meant to vote to reopen, and not use my code-golf golden hammer... If people really insist it's a duplicate vote to close again.

Yeah I would now agree that this ain't a duplicate although some of the entries might be just a modification of the previous ones.

I think it's close enough to be a duplicate, but anyone who previously voted to close is now unable to do so (it won't let me vote again). So I think @orlp should close it.

@mbomb007 Nobody except you should vote to close because you think the challenge should be closed. Please don't tell people how to vote.

@Dennis You're misunderstanding mbomb007 I believe. mbomb007 (and others) did in fact vote to close, and it got 5 votes. I disagreed so voted to reopen, but I didn't realize this would instantly reopen due to my golden codegolf badge. Hence my comment and now his (he can't vote on this question anymore).

@Dennis https://codegolf.stackexchange.com/review/close/history

Yes, I saw that. While it's unfortunate that you accidentally hammered your own question, you shouldn't be compelled to cast a vote you disagree with.

I don't think marking as dupe is fair. Printing explicitly takes much more work than counting.

@Dennis If they do VTC according to mbomb007's comment, they should agree with that. So no problem.

JavaScript (ES6), 35 bytes
Saved 1 byte thanks to @tsh
f=(n,s)=>n--?f(n,n-~s)+f(n,n+~s):!s

Try it online!

Wolfram Language (Mathematica), 33 bytes
Count[{1,-1}~Tuples~#.Range@#,0]&

Counts the n-tuples of 1 and -1 whose dot product with Range[n] is 0.
Try it online!

Haskell, 42 bytes
f n=sum[1|0<-sum<$>mapM(\x->[x,-x])[1..n]]

Try it online!
This is 2 1 byte shorter than any recursive function that I could write.

05AB1E, 10 bytes
X®‚sã€ƶO_O

Try it online!
Explanation
X®‚          # push [1,-1]
   sã        # cartesian product with input
     €ƶ      # multiply each element in each list with its 1-based index
       O     # sum each list
        _    # logical negation of each sum
         O   # sum

The code.. it's staring at me. What do I do?

C (gcc), 45 62 52 50 bytes
f(n,r){n=n?f(n-1,r+n)+f(n-1,r-n):!r;}F(n){f(n,0);}

Port of Kevin Cruijssen's Java 8 answer.
Try it online here.
Note that due to the improvements suggested in the comments, the code produces undefined behaviour to the point of not working when compiled with clang.
Thanks to etene for golfing 3 bytes.
Thanks to Kevin Cruijssen for golfing 10 more bytes.
Thanks to Christoph for golfing another 2 bytes.
Ungolfed version:
f(n, r) { // recursive function - return type and parameter type are omitted, they default to int
    n = // instead of returning, we set n - dirty trick
        n ? // if n is not 0, recurse
        f(n-1,r+n) // +n
       +f(n-1,r-n) // -n
        !r; // else if r != 0 return 0 else return 1
}
F(n) { // function to start the recursion; again implicitly int(int)
    n = f(n, 0); // call the recursive function; this time we simply don't return
}

You could shave off 3 bytes by replacing r?0:1 with !r. 42 bytes

It looks like you're taking additional input here in order to set the initial value of r, which isn't permitted.

@Shaggy Edited. Thanks for pointing that out to me, still learning the rules :D

@etene Well spotted, thank you!

Why did you create a port of my Java answer? Creating a port of @Arnauld's JavaScript (ES6) answer is shorter. ;) Also, you can get rid of the return in C: f(n,s){n=n--?f(n,s-~n)+f(n,s+~n):!s;}F(n){n=f(n,0);} Try it online 52 bytes

@KevinCruijssen better yet the second n= isn't necessary either: f(n,r){n=n?f(n-1,r+n)+f(n-1,r-n):!r;}F(n){f(n,0);}.

@KevinCruijssen I used your version because frankly I don't understand Arnauld's :P However with your improvements (thanks for teaching me that dirty return trick), my port of your answer is down to 52 bytes as well – no worse than your suggested version.

@O.O.Balance the trick is two's complement. This means that -x = ~x+1and therefore ~x = -x-1.

@Christoph thanks for explaining and shaving another 2 bytes. Unfortunately it now only works with gcc :-(

@Christoph Ah, didn't knew it was possible without the n=. I don't program that much in C, so thanks for learning me something new. :) O.O.Balance, as for an explanation of Arnauld's answer that I linked: s-~n and s+~n are shorter variations of s+n+1 and s-n-1 (here is the relevant tip). And !r is a shorter variation for r==0?1:0 (so if r is any positive or negative integer, return 0, otherwise (it's zero), return 1).

@KevinCruijssen Thanks for the link.

The reason the implicit return works is because on x86 CPU's, C will put integer return values in the EAX/RAX register. Since this register is never modified, it will still contain the right result after returning from F. If you try returning a value larger than int, this trick might not work.

@YoYoYonnY Thanks for explaining.

05AB1E, 9 8 bytes
Thanks to Emigna for saving a byte!
Code:
LæO·sLO¢

Uses the 05AB1E encoding. Try it online!
Explanation
L           # Create the list [1, 2, .., input]
 æ          # Compute the powerset of this list
  O         # Sum each list
   ·        # Double each element
    sLO     # Compute the sum of [1, 2, .., input]
       ¢    # Count the number of occurrences

MATL, 14 13 bytes
[la]Z^G:!Y*~s

Thanks to @Giuseppe for saving 1 byte!
Try it online! Or verify all test cases.
Explanation
Consider n = 3 as an example. Stack is shown upside down, that is, newest appears below.
[la]   % Push array [1 -1]
       % STACK: [1 -1]
Z^     % Cartesian power with inplicit input n
       % STACK: [ 1  1  1
                  1  1 -1
                  1 -1  1
                  1 -1 -1
                 -1  1  1
                 -1  1 -1
                 -1 -1  1
                 -1 -1 -1]
G:     % Push n, range: gives [1 2 ... n]
       % STACK: [ 1  1  1
                  1  1 -1
                  1 -1  1
                  1 -1 -1
                 -1  1  1
                 -1  1 -1
                 -1 -1  1
                 -1 -1 -1],
                 [1  2  3]
!      % Transpose
       % STACK: [ 1  1  1
                  1  1 -1
                  1 -1  1
                  1 -1 -1
                 -1  1  1
                 -1  1 -1
                 -1 -1  1
                 -1 -1 -1],
                 [1
                  2
                  3]
Y*     % Matrix multiplication
       % STACK: [6
                 0
                 2
                -4
                 4
                -2
                 0
                -6]
~      % Logical negation
       % STACK: [0
                 1
                 0
                 0
                 0
                 0
                 1
                 0]
s      % Sum of vector. Implicit display
       % STACK: 2

Jelly, 8 bytes
ŒPS€ċÆṁ$

Try it online!
How it works
ŒPS€ċÆṁ$  Main link. Argument: n

ŒP        Take the powerset of [1, ..., n].
  S€      Take the sum of each subset.
       $  Combine the two links to the left into a monadic chain.
     Æṁ       Compute the median of the sums, i.e, (1 + ... + n)/2.
    ċ         Count the occurrences of the median.

APL (Dyalog), 31 22 bytes
9 bytes saved thanks to @H.PWiz
1⊥0=⊂∘⍳+.×¨∘,3-2×∘⍳⍴∘2

Try it online!

Java 8, 72 71 70 bytes
n->f(0,n)int f(int r,int n){return n>0?f(r+n,--n)+f(r+~n,n):r==0?1:0;}

Port of @Arnauld's JavaScript (ES6) answer.
-2 bytes thanks to @OlivierGrégoire.
Try it online.
Explanation:
n->                 // Method with integer parameter and integer return-type
  f(0,n)            //  Call the recursive method with 0 and this parameter

int f(int r,int n){ // Recursive method with integer as both two parameters and return-type
  return n>0?       //  If `n` is not 0 yet:
    f(r+n,--n)      //   Recursive call with `r+n` (and `n` lowered by 1 first with `--n`)
    +f(r+~n,n)      //   + Recursive call with `r-n` (and `n` also lowered by 1)
   :r==0?           //  Else-if `r` is 0
     1              //   Return 1
    :               //  Else:
     0;}            //   Return 0

Python 2, 74 bytes
def f(n):l=k=1;exec"l+=l<<n*k;k+=1;"*n;return(l>>n*n*-~n/4)%2**n*(~-n%4>1)

More of a fun submission, direct generating function computation.

Octave  (with Communications Package), 39 bytes
@(n)sum((2*de2bi(0:2^n-1)-1)*(1:n)'==0)

Try it online!
Explanation:
Take a range 0 ... n^2-1 and convert it to binary. This gives a matrix with all combinations of 0 and 1. Multiply by 2 and subtract 1 to get a matrix with all combinations of -1 and +1.
Take the dot-product with a range 1 ... n to get all combinations of ±1 ± 2 ... ±n. Count how many are zero.
Basically the same thing, same byte count:
@(n)nnz(~((2*de2bi(0:2^n-1)-1)*(1:n)'))

Haskell, 55 bytes
A straightforward approach of computing all those sums and checking how many are zero.
f 0=[0]
f n=[(n+),(n-)]>>=(<$>f(n-1))
g x=sum[1|0<-f x]

Try it online!
EDIT: @H.PWiz has a shorter and way more elegant solution using mapM!

Python 2 and 3, 50 bytes
Recursive approach like most of the answers:
f=lambda n,r=0:f(n-1,r+n)+f(n-1,r-n)if n else r==0

Try it online
The double recursive call takes too much bytes... There's probably a way to simplify it.

Bash + GNU utilities, 63 bytes
Bash can probably do better than this with recursive functions, but I can't resist this sort of eval/escape/expansion monstrosity:
p=eval\ printf\ %s
$p\\\\n \$[$($p \\\{+,-}{1..$1})]|grep -c ^0

Try it online!

Update: I don't think bash can do better with recursive functions. This is the best I could do for a score of 90.  eval hell it is then.

Brachylog, 12 bytes
⟦₁{{ṅ|}ᵐ+0}ᶜ

Try it online!
Explanation
⟦₁               The range [1, …, Input]
  {       }ᶜ     Count the number of times the following predicate succeeds on that range:
   {  }ᵐ           Map for each element of the range:
    ṅ                Negate
     |               Or do nothing
        +0         The sum of the elements after the map is 0

Octave, 42 bytes
@(n)sum((dec2bin(0:2^n-1)*2-97)*(1:n)'==0)

Try it online!

Well, +1 I guess. :) Hadn't seen this when I posted mine.

Heh. I hadn't seen yours either until now

J, 32 bytes
1#.0=1#.1+i.*"1[:<:@+:@#:[:i.2^]

Try it online!
There is certainly much room for golfing. Exlpanation will follow.

Haskell, 41 bytes
(%0)
n%k|n<1=0^k^2|m<-n-1=m%(k+n)+m%(k-n)

Try it online!

Nice, I had the same, but 0^abs k.

Jelly, 10 bytes
RżN$ŒpS€ċ0

Try it online!

Perl 5, -p 35 bytes
#!/usr/bin/perl -p
$_=grep!eval,glob join"{+,-}",0..$_

Try it online!

Pari/GP, 30 bytes
n->Pol(prod(i=1,n,x^i+x^-i))%x

Try it online!

Stax, 9 bytes
è%é┐╬@₧╠¬

Run and debug it
 One of the shortest answers so far   defeated by Jelly.
I feel that checking explicitly which signs sum to zero is not very golfy, so instead I take the powerset and check how many sets in the powerset have the sum of half the nth triangular number. This method is, not surprisingly, of the same time complexity as checking which signs sum to zero.
ASCII equivalent:
RS{|+Hmx|+#

Prolog (SWI), 99 bytes
p(0,0,1).
p(0,_,0).
p(X,Y,Z):-A is X-1,B is Y+X,p(A,B,C),D is Y-X,p(A,D,E),Z is C+E.
X*Y:-p(X,0,Y).

Try it online!

Pyth, 14 13 bytes
lf!s.nT*F_BRS

Try it here
Explanation
lf!s.nT*F_BRS
            SQ  Take the list [1, ..., <implicit input>].
         _BR    Get the pairs [[1, -1], [2, -2], ...].
       *F       Take the Cartesian product.
 f!s.nT         Find the ones where the flattened sum is 0.
l               Take the length.

CJam, 25 bytes
ri,:)_Wf*:a.+:m*:e_1fb0e=

Try it online!
This is a fairly direct translation of @emigna's 05AB1E solution. It's certainly golfable.

Pyth, 10 bytes
/mysdySQsS

Try it online. Alternatively, verify all test cases at once.
Explaination:
/mysdySQsS    Implicit: Q=input()
      SQ      Generate range [1...Q]
     y        Generate powerset of above
 m            Map d in the above over...
  ysd         ... double the sum of d
        sS    Sum of range [1...Q] (final Q is implicit)
/             Count the matches (implicit output)

J, 28 bytes
(*>:){1j3#1+//.@(*/)/@,.=@i.

Uses the other definition from OEIS where a(n) = coefficient of x^(n(n+1)/4) in Product_{k=1..n} (1+x^k) if n = 0 or 3 mod 4 else a(n) = 0.
Try it online!
Explanation
(*>:){1j3#1+//.@(*/)/@,.=@i.  Input: n
                          i.  Range [0, n)
                        =     Self-Classify. Forms an identity matrix of order n
          1           ,.      Stitch. Prepend 1 to each row
                    /         Reduce using
                                Convolution
                 */               Product table
           +//.                   Sum along anti-diagonals
      1j3#                    Copy each once, padding with 3 zeroes after
     {                        Index at n*(n+1)
  >:                            Increment n
 *                              Times n

Husk, 9 bytes
#½Σḣ¹mΣṖḣ

Try it online!
Explanation
#½Σḣ¹mΣṖḣ  Implicit input
        ḣ  [1..input]
       Ṗ   Powerset
     mΣ    Sum each list
#          Count occurrence of
   ḣ¹        [1..input]
 ½Σ          Half of sum

Gol><>, 26 bytes
:IFPlMF2K+}:@-}||0lMF$z+|h

Try it online! or Run test cases from 1 to 16!
How it works
:IFPlMF2K+}:@-}||0lMF$z+|h

Main outer loop
:IFPlMF ...... ||
:        Duplicate top; effectively generate two explicit zeroes
         Top is the loop counter `i`;
         the rest is the generated 2**i sums
 I       Take input as number
  F ........... |  Pop n and loop n times
   P     i++
    lM   Push stack length - 1, which is 2**(i-1)
      F ...... |   Loop 2**(i-1) times

Main inner loop: generate +i and -i from 2**(i-1) previous sums
2K+}:@-}
          Stack: [... x i]
2K        [... x i x i]    Copy top two
  +}      [x+i ... x i]    Add top two and move to the bottom
    :@    [x+i ... i i x]  Duplicate top and rotate top 3
      -}  [i-x x+i ... i]  Subtract and move to the bottom

Counting zeroes
0lMF$z+|h
0lM        Push zero (zero count) and 2**n (loop count)
   F...|   Loop 2**n times
    $z+    Swap top two; Take logical not; add to the count
        h  Print top as number and halt


text:
Pi got your number
Challenge :
\$\pi\$ is supposed to be infinite. That means every number is contained inside the decimal part of \$\pi\$.
Your task will be to take a positive integer on input and return the position of this number in \$\pi\$ digits on output.
For example, if the input is 59, we'll return 4
Here is why : we will look for the number 59 in the digits of \$\pi\$
3.14159265...
     ^^

The value starts at the 4th digit, so the output will be 4.
Some other examples :
input : 1      output : 1
input : 65     output : 7
input : 93993  output : 42
input : 3      output : 9

Rules :

You don't have to handle digits that doesn't exist within the first 200 digits
Standard loopholes are, as always, forbidden.
This is codegolf, so the fewer bytes wins.

Numbers with the property you mention are known as normal numbers. An infinite decimal expansion, even if non-periodic, doesn't imply normality. 0.101001000100001... is a counterexample.

And, absolutely, Pi is not supposed to be infinite. It's decimal representation, however, have infinite digits.

@Dennis Normal is a much stronger condition (all-uniform vs all-exist)

Related

@user202729 Shows how much I know about number theory. :/

I was about to incorrectly type the same (numbers like that being normal) :-D

Can we take input as a string?

@Dennis yes, there is no restiction for the input

Related

Are we allowed to output the 0-indexed n'th index? So the text cases would return 0, 6, 41, 8 instead of 1, 7, 42, 9.

@rafa11111 I agree. We should abandon integers and use numbers in base-PI. Then integers will have infinite digits, instead.

"You don't have to handle digits that doesn't exist within the first 200 digits" - do you mean input integers that don't?

@mbomb007 that's a lovely idea but, unfortunately, somebody already thought on this... https://en.wikipedia.org/wiki/Non-integer_representation#Base_%CF%80

@rafa11111 Yeah, I know. I've been looking at related information.

@rafa11111 https://codegolf.stackexchange.com/q/76062/34718

I say allow for negative numbers, with the understanding that negative means "signed" so it's the first occurrence of that number where it is immediately preceded by 1.

From https://en.wikipedia.org/wiki/Normal_number: It is widely believed that the (computable) numbers √2, π, and e are normal, but a proof remains elusive. (emphasis mine) π only probably contains every possible sequence of digits.

I improved formatting, feel free to take it back if you don't want it.

Python 2, 69 75 71 67 bytes
Saved 4 bytes due to caird coinheringaahing.
x=p=1333
while~-p:x=p/2*x/p+2*10**200;p-=2
print`x`.find(input(),1)

Not finding 3 at position zero cost 6 2 bytes. Input is given as a string.
Try it online!

Unbounded Version
Python 2, 224 bytes
def g():
 q,r,t,i,j=1,0,1,0,1
 while True:
  i+=1;j+=2;q,r,t=q*i,(2*q+r)*j,t*j;n=(q+r)/t
  if n*t>4*q+r-t:yield n;q,r=10*q,10*(r-n*t)
a=input()
l=len(`a`)
s=z=10**l;i=1-l
p=g().next;p()
while s!=a:s=(s*10+p())%z;i+=1
print i

Using an unbounded spigot based on the same formula used above.
Try it online!

Faster Version
from gmpy2 import mpz
def g():
  # Ramanujan 39, multi-digit
  q, r, s ,t = mpz(0), mpz(3528), mpz(1), mpz(0)
  i = 1
  z = mpz(10)**3511
  while True:
    n = (q+r)/(s+t)
    if n == (22583*i*q+r)/(22583*i*s+t):
      for d in digits(n, i>597 and 3511 or 1): yield d
      q, r = z*(q-n*s), z*(r-n*t)
    u, v, x = mpz(1), mpz(0), mpz(1)
    for k in range(596):
      c, d, f = i*(i*(i*32-48)+22)-3, 21460*i-20337, -i*i*i*24893568
      u, v, x = u*c, (u*d+v)*f, x*f
      i += 1
    q, r, s, t = q*u, q*v+r*x, s*u, s*v+t*x

def digits(x, n):
  o = []
  for k in range(n):
    x, r = divmod(x, 10)
    o.append(r)
  return reversed(o)

a=input()
l=len(`a`)
s=z=10**l;i=1-l
p=g().next;p()
while s!=a:s=(s*10+p())%z;i+=1
print i

A much faster unbounded spigot, based on Ramanujan #39.
Try it online!

Nice, neither hardcodes nor use built-in (because Python doesn't have any)

This fails for input 3 (expected 8, but outputs 0). You need to ignore the 3 before the decimal comma.

@KevinCruijssen missed that, thanks.

I think you are allowed to remove the +1 and output the 0-indexed result, but not sure. I've asked OP to clarify, since I do the same in my Java answer.

Trivial 4 byte reduction

@Dennis 31 needs to match at 137 :/

Which approximation algorithm is this? Is it one listed here? https://en.wikipedia.org/wiki/Approximations_of_%CF%80

@Sphinxxx it's the resullt of apply the Euler transform to the Leibniz series. I've posted a derivation in a previous post.

Husk, 5 bytes
€tİπd

Try it online!
Explanation
€tİπd                              59
    d  Convert to base-10 digits   [5,9]
  İπ     The digits of pi          [3,1,4,1,5,9..]
 t       Remove the first element  [1,4,1,5,9,2..]
€      Index of the sublist        4

Ridiculous - but I have to admit I'm impressed.

With golfing languages it's usually a good idea to add an explanation, since someone who doesn't know the language won't be able to read it. If I understand correctly it's: Take the index of (€) with the first item (the leading 3) removed (t) of the digits of PI (İπ), convert it to base-10 (d) and output to STDOUT (implicitly).

Agreed, I have no idea what I'm looking at.

Is İπ a lazy representation of the digits? Otherwise, whats the precision?

@gggg looks like it is a lazy representation example, verification

@gggg İπ is an infinite list of digits, created with an unbounded spigot source

Excel, 212 bytes
=FIND(A1,"14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196")

Excel only handles 15 decimal places so pi is just hard-coded. This should be a pretty weak upper bound for this challenge.

I'm sorry to comment on my own post, but can some of the upvoters tell me why they like this answer? It's as golfed as it can be in an Excel formula but it's very long and not at all clever.

I like this because it doesn't rely on golfing languages which have builtins to calculate pi to an arbitrary decimal place.  It may not be creative, but it's practical (not that practicality matters here).

As the question doesn't specify that the input or answer have to be base 10, could you golf this by using CONCAT and a BBP formula to calculate the first 200 digits of π-base16 and search in Hexadecimal instead?  (Don't have 365, so can't test)

Office 365 only: using CONCAT, CODE and MID I reduced the PI string from 202 characters (inc quotes) to 143: CONCAT(CODE(MID(".ÜÁ£ÙÏ ¦®š«¦ Ï²œÔ“ÇÅ§ÝËŠº”á±¬»—‡ÑÀ†œ¾ˆãÖœƒ°™¢•‘†ÏÒŽÐÖ³ ÒžÂ¯‰¦¬¼ß²º–ŸÈµ»¨Ñœ°‹‘‚ÔŠ›ÝÕ•Š·»À®–ÞÙ¶ÝƒÑà",2*ROW(A1:A100)-1,2))-32)

@Chronocidal That's impressive but I can't verify that in Excel Online, which is all I can access. Does it need to be entered as an array formula? That would explain it because Excel Online doesn't allow entering array formulas. If you post yours as a separate answer, I'll definitely vote for it.

Unfortunately, I also can't properly verify it (I tested by using 100 rows and CONCATENATE(A1,A2,A3..A100) o_O), but the examples on Office.com seem indicate that it doesn't need to be entered as an array formula...  Can anyone with Office365 either disprove or confirm & post as an answer?

Testing with Office365, it looks like it outputs 14 regardless of the input?

@MatthewSchlachter Thanks for testing! :)  Sounds like it's only processing the first character though...  :(  If you press [Ctrl]+[Shift]+[Enter] to turn it into an Array Formula, does it still give "14", or output all 200 digits?

@Chronocidal - your discussion on this made me want to try a whole bunch of string compression methods for this, so I did - link. I found that for this case, sticking to ASCII-only compression is preferred for this problem, and found four equivalent 148 byte solutions that you can see in Approach 5. I also found two 96 char, 177 byte solutions using triple byte unicode characters.

Java 8, 615 217 202 184 182 166 165 bytes (calculated 999 200 digits)
n->{var t=java.math.BigInteger.TEN.pow(200);var r=t;for(int p=667;p-->1;)r=t.valueOf(p).multiply(r).divide(t.valueOf(p-~p)).add(t).add(t);return(r+"").indexOf(n,1);}

1-indexed
Try it online.
Java's builtin Math.PI has a precision of 15 decimal values, like many other languages. To have more digits, you'll have to calculate them yourself with BigIntegers or BigDecimals. This above is a way to do it.. Maybe someone can golf this below 211 bytes, lol..
EDIT: Created a port of @primo's Python 2 answer (make sure to upvote him!), so calculating being shorter than hard-coded is not so far-fetched anymore. Just 7 more bytes to golf for it to be shorter.
-15 bytes thanks to @Neil, making it shorter than the hard-coded answer below!
-36 bytes thanks to @primo.
-1 byte changing java.math.BigInteger t=null,T=t.TEN.pow(200),r=T; to var T=java.math.BigInteger.TEN.pow(200);var r=T;, because var is 1 byte shorter than null (gotta love the new Java 10).
Explanation:
n->{                            // Method with String parameter and integer return-type
  var t=java.math.BigInteger.TEN.pow(200);
                                //  Temp BigInteger with value 10^200
  var r=t;                      //  Result BigInteger, also starting at 10^200
  for(int p=667;                //  Index-integer, starting at 667
      p-->1;)                   //  Loop as long as this integer is still larger than 1
                                //  (decreasing `p` by 1 before every iteration with `p--`)
    r=                          //   Replace the Result BigInteger with:
      t.valueOf(p)              //    `p`
       .multiply(r)             //    multiplied by `r`,
       .divide(t.valueOf(p-~p)) //    divided by `2*p+1`
       .add(t).add(t);          //    And add 2*10^200
  return(r+"")                  //  Convert the BigInteger to a String
    .indexOf(n,                 //  And return the index of the input,
               1);}             //  skipping the 3 before the comma

Java 8, 211 bytes (hard-coded 200 digits)
"14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196"::indexOf

0-indexed
Try it online.

!p.equals(t.ONE) perhaps? Also, indexOf(n,1)-1 works I think. Or save 2 bytes and make it 1-indexed.

Not sure how I missed the first, but the second I really need to remember. Didn't knew there was an indexOf method that skips the first m characters. TIL, thanks!

How about keeping p an integer?

@primo Thanks! 18 bytes saved thanks to you! (After your port already saved about 400 bytes.. ;p)

You can also decrement p by one each time (for(int p=667;p-->1;)), and then multiply by p and divide by p-~p.

If you redefine T as t.TEN.pow(200), then you can just .add(T).add(T).

@primo But how about r=T? r should start at 2, shouldn't it?

The initial value of r can literally be anything, although extreme values will require more iterations. The best seed (fewest iterations) is actually 4e200.

MATL, 16 15 bytes
YP8WY$4L)jXfX<q

Try it online!
Explanation
YP     % Push pi as a double
8W     % Push 2^8, that is, 256
Y$     % Compute pi with 256 significant digits using variable-precision arithmetic
       % The result as a string
4L)    % Remove first character. This is to avoid finding '3' in the integer part
       % of pi
j      % Push input as a string
Xf     % Strfind: gives array of indices of occurrences of the input string in the
       % pi string
X<     % Mimimum
q      % Subtract 1. Implicitly display

Very nice and short ! Can you explain how it works ?

@Therandomguy Sure, explanation added

05AB1E, 6 bytes
₁žs¦¹k

Try it online!
How?
₁        push 256
 žs      push pi to 256 places
   ¦     remove the leading 3
    ¹    push the input
     k   index inside that string

If I get the similar 6-byte solution in the same language, after you, do I delete my answer?

@nicael usually it doesn't matter, but your solution fails for 3 anyway

Oh, indeed, thnks

R + numbers package, 52 bytes
regexec(scan(),substring(numbers::dropletPi(200),3))

Try it online!
dropletPi computes the first 200 decimal digits of pi but includes a 3. at the beginning, so we strip that out with substring and then match with regexec, which returns the index of the match along with some metadata about the match.

Maybe regexpr(scan(),numbers::dropletPi(200))-2?

@djhurio that doesn't work because we have to match in the digits after the decimal point. That was my first thought as well but that case ruins it. Maybe an "if"?

I do not see a problem here. Non of the input will contain 3. (I assume we deal with integers not reals in input). The test examples work with this.

@djhurio right but regexpr(3,numbers::dropletPi(200))-2 returns -1  when it should return 9, try it

Jelly, 23 bytes
⁵*⁹Ḥ;ȷḊ+J$¤×⁹:2¤:ɗ\SṾḊw

A monadic link accepting a list of characters (the integer to find) and returning the index. Works for inputs contained within the first 252 digits of the decimal part of π.
Try it online!
How?
This uses the Leibniz formula for π to calculate the first 253 digits including the leading 3 (plus four trailing incorrect digits). The leading 3 is then dropped and the index of the input is found:
⁵*⁹Ḥ;ȷḊ+J$¤×⁹:2¤:ɗ\SṾḊw - Link: list of characters
⁵                       - literal ten
  ⁹                     - literal 256
 *                      - exponentiate = 10000...0 (256 zeros)
   Ḥ                    - double       = 20000...0
          ¤             - nilad followed by links as a nilad:
     ȷ                  -   literal 1000
      Ḋ                 -   dequeue -> [2,3,4,5,...,1000]
         $              -   last two links as a monad:
        J               -     range of length -> [1,2,3,4,...,999]
       +                -     addition (vectorises) -> [3,5,7,9,...,1999]
    ;                   -   concatenate -> [20000...0,3,5,7,9,...,1999]
                  \     - cumulative reduce with:
                 ɗ      -   last three links as a dyad:
               ¤        -     nilad followed by link(s) as a nilad:
            ⁹           -       chain's right argument (the right of the pair as we traverse the pairs in the list -- 3, 5, 7, 9, ...)
              2         -       literal two
             :          -       integer division (i.e. 1, 2, 3, ...)
           ×            -     multiply (the left of the pair, the "current value", by that)
                :       -   integer divide by the right argument (i.e. 3, 5, 7, 9, ...)
                   S    - sum up the values (i.e. 20000...0 + 66666...6 + 26666...6 + 11428...2 + ... + 0)
                    Ṿ   - un-evaluate (makes the integer become a list of characters)
                     Ḋ  - dequeue (drop the '3')
                      w - first (1-based) index of sublist matching the input

If you prefer a list of digits as input use ⁵*⁹Ḥ;ȷḊ+J$¤×⁹:2¤:ɗ\SDḊw (also 23), while if you really want to give it an integer use ⁵*⁹Ḥ;ȷḊ+J$¤×⁹:2¤:ɗ\SDḊwD (for 24).

You mean Euler's transform applied to the Leibniz formula. Calculating 252 digits with the Leibniz formula would take a wee bit longer than most people would be willing to wait.

Yes it would take a long time in raw form (it's still "using the Leibniz formula" I believe!)

BASH (GNU/Linux), 75 67 66 bytes
Saved 1 byte thanks to Sophia Lechner, and 7 bytes thanks to Cows quack.
a=`bc -l<<<"scale=999;4*a(1)"|tail -c+2|grep -ob $1`;echo ${a%%:*}

This is a shell script that takes a single argument, which is the number. Test with
$ bash <script-path> 59
4

This script first executes a pipeline of three commands:
bc -l<<<"scale=999;4*a(1)"|    #produce pi with its first 999 fractional digits
tail -c+2|                     #cut off the "3."
grep -ob $1                    #compute the byte offsets of our argument in the string

The result of this pipeline is assigned to the shell variable a, which is then echoed out with anything but the first number removed:
a=`...`;         #assign the result of the pipeline to a variable
echo ${a%%:*}    #cleave off the first : character and anything following it

Unfortunately, bc has the tendency to break output lines when they become too long. This may lead to wrong results if the number to be found is not on the first line. You can avoid that by setting the environment variable BC_LINE_LENGTH:
export BC_LINE_LENGTH=0

This deactivates the line breaking feature completely.

Obviously, the last two commands may be omitted if other output is tolerated.
This gives a count of 48 bytes:
bc -l<<<"scale=999;4*a(1)"|tail -c+2|grep -ob $1

With the resulting output:
$ bash <script-path> 59
4:59
61:59
143:59
179:59
213:59
355:59
413:59
415:59
731:59
782:59
799:59
806:59
901:59
923:59
940:59
987:59

Nice! You don't need that space between -l and <<< though.

You can convert to a program and use sed to save some bytes, Try it online!

@Cowsquack Wouldn't I need to include a shebang line in the byte count then?

@cmaster shebang lines are not included in byte counts for any languages

@Cowsquack Thanks for the suggestion. However, if you allow for additional output, you might as well leave out the sed as well (see the second part of my answer). Nevertheless, transforming to a program gave me 7 bytes, so thanks for that! I have also replaced the tr/head combo with shell variable magic now to save another byte.

@SophiaLechner Cool, I would not have thought that's possible. Thanks.

Nice. I had to look up bc to figure out what it was and also that a is the arctan function.

@gggg Yeah, bc is one of those really powerful tools with a rather retro-charm to them that are usually overlooked completely. Today, one would probably name that a() function just arctan(), but that would have cost me another five bytes...

Haskell, 208 120 bytes
a=1333
x=tail$show$foldr(\p x->p`div`2*x`div`p+2*10^200)a[3,5..a]
x!n|take(length n)x==n=0|1<2=1+tail x!n
f n=1+x!show n

Try it online!
Many thanks to Jonathan Allan for his suggestions!
Old version (208 bytes)
(+1).((tail$g(1,0,1,1,3,3))!)
g(q,r,t,k,n,l)=([n:g(10*q,10*(r-n*t),t,k,div(10*(3*q+r))t-10*n,l)|4*q+r-t<n*t]++[g(q*k,(2*q+r)*l,t*l,k+1,div(q*(7*k+2)+r*l)(t*l),l+2)])!!0
x!n|take(length n)x==n=0|1<2=1+tail x!n

I actually don't know how the code above works; I've taken it from this paper and all I implemented was the lookup part.
g(1,0,1,1,3,3) returns the digits of pi and is surprisingly efficient (it computes 10 000 digits on tio.run in less than 4s).
The input is a list consisting of the digits of the number to be found.
Try it online!

My guess is that  the Leibniz formula will be far shorter.

@JonathanAllan Thanks! I will give it a try. I absolutely love this site! I've learned so much from you, guys! :)

@JonathanAllan I tried to approximate pi using l=4*sum[((-1)**x/(2*x+1))|x<-[0..1e6]], but that takes 5s to run and the 7th digit is already wrong. So it might not be feasible to compute 200 digits. It was an interesting exercise anyway, so thanks!

You'd want to use the Euler transform (see my Jelly answer or primo's Python answer)

In reference to the paper you linked, you might be interested in this post, in which I re-implement the code found in this paper without "deliberate obfuscation." It's also quite a bit simpler (shorter) as a result. See method g1_ref in section Faster Unbounded Generators. The code is python.

SmileBASIC, 179 164 bytes
INPUT I$FOR I=0TO 103Q$=Q$+STR$(ASC("\A#YO &.+& O2TGE']KiRa1,;N(>VYb>P0*uCb0V3 RB/]T._2:H5;(Q0oJ2)&4n7;@.^Y6]&"[I]))NEXT?INSTR(Q$,I$)+1

Digits of pi are hardcoded and packed into the ascii values of characters.
14 -> CHR$(14), 15 -> CHR$(15), 92 -> \, 65 -> A, 35 -> #.
The string contains unprintable characters, so here are the bytes written in hexadecimal: 0E 0F 5C 41 23 59 4F 20 26 2E 1A 2B 26 20 4F 32 1C 54 13 47 45 27 5D 4B 69 52 00 61 31 2C 3B 17 00 4E 10 28 3E 56 14 59 62 3E 50 03 30 19 03 2A 75 00 43 62 15 30 00 56 33 20 52 1E 42 2F 00 5D 54 2E 00 5F 32 3A 16 1F 48 35 3B 28 51 1C 30 6F 4A 32 1C 29 00 1B 00 13 26 34 6E 37 3B 40 2E 16 5E 59 36 5D 00 26 13 06
In decimal, you can see the digits of pi: 14 15 92 65 35 89 79 32 38 46 26 43 38 32 79 50 28 84 19 71 69 39 93 75 105 82 0 97 49 44 59 23 0 78 16 40 62 86 20 89 98 62 80 3 48 25 3 42 117 0 67 98 21 48 0 86 51 32 82 30 66 47 0 93 84 46 0 95 50 58 22 31 72 53 59 40 81 28 48 111 74 50 28 41 0 27 0 19 38 52 110 55 59 64 46 22 94 89 54 93 0 38 19 6

If you post the complete code, it would make it easier to verify your answer.

I can't post it because there are invalid characters that are removed/not displayed. I guess I can post the ascii codes though.

You could post a hexdump, using xxd for example.

Japt, 186 177 bytes
`nqnrvosrpruvtvpopuqsosqppÕÝvr¶uuqnvtnsvpvvptrnmruomvtqvqqrvopmÉæqÛàÑ$vvÔàmpqupqm¡vuqum«rnpopmssqtmvpuqqsmvrrmruoopÌÊprvqÛ$uqunnqr¶uqn¶tmnvpÔnmrrrvsqqsoovquvrqvpmpunvs`®c -#mÃbU

Since Japt shares Javascript's 15-digit Pi constraint and shoco, the encoding used by Japt, doesn't encode numbers, some shenanigans are required for compression.
Shortly explained, the beginning is the below string in encoded form:
"nqnrvosrpruvtvpopuqsosqppupotvrmouuqnvtnsvpvvptrnmruomvtqvqqrvopmtunsqmsousomuvvusoumpquorpqonntmstvuonqumusrnpouopmssqtmvpuqqsmvrrmruoopntorprvqmunouqunnntqrmouqnmotmnvpuronnmrrrvsqqsoovquvrqvpmpunvs"

Which is a string where each letter is 'm' + corresponding digit of pi. I tested the whole alphabet and that letter gives the best compression by a few bytes.
Backticks tell Japt to decode the string. The rest of it is pretty straightforward:
®c -#mÃbU
®          // Given the above string, map each letter
 c         // and return its charcode
   -#m     // minus the charcode of 'm', 109.
      Ã    // When that's done,
        bU // find the index of the implicit input U.

Outputs 0-based index of the matching fragment.
Shaved another two bytes off thanks to Oliver.
Try it online!

Clever idea! You can replace £X with ® and }  with Ã

@Oliver Thanks a lot for those, I'm still learning Japt so all help is very appreciated.

You've been doing great so far! I was curious to see if there was a better offset than 109. I made a bruteforcer, and it turns out 109 is optimal. Nicely done :)

@Oliver Thanks for that, I simply tried the whole a-z range manually since it wasn't too much work. :P

JavaScript, 197 187
-10: Thanks, Neil!
x=>"50ood0hab15bq91k1j9wo6o2iro3by0h94bg3geu0dnnq5tcxz7lk62855h72el61sx7vzsm1thzibtd23br5tr3xu7wsekkpup10cek737o1gcr6t00p3qpccozbq0bfdtfmgk".replace(/.{9}/g,a=>parseInt(a,36)).search(x)+1

Takes a series of nine-digit base-36 integers, converts them to base 10, and concatenates them to create the first 200 digits of pi.

Nice, you blow my attempts at encoding the data out of the water, your approach saves 38 bytes on the raw data.

+1 - I was about to post the exact same approach.

Use x=>'50...'.replace(/.{9}/g,a=>parseInt(a,36)).search(x)+1 to save 10 bytes.

Charcoal, 27 15 bytes
Ｉ⊖∨⌕Ｉ▷N⟦≕Piφ⟧θχ

Try it online! Link is to verbose version of code. Works up to nearly 1000 digits. Explanation:
        ≕Pi     Get variable `Pi`
           φ    Predefined variable 1000
     ▷N⟦    ⟧   Evaluate variable to specified precision
    Ｉ           Cast to string
             θ  First input
   ⌕            Find
              χ Predefined variable 10
   ∨             Logical OR
  ⊖              Decrement
 Ｉ               Cast to string
                 Implicitly print

fixed, 13 bytes. side note: this feels really cheaty :P

actually fixed, 13 bytes. uses implicit input. (not intended behavior but it seems more useful than any other way). also could you link to an example of the fill bug?

@ASCII-only Fill weirdness - why does the cursor end up there?

:| oh i have no idea i should fix that asap

nvm i'm an idiot, committed fix.

this will work after Dennis pulls

First time doing code golf. Use delegates and lambda expressions to reduce the function calls. V2 shorten class name into a single byte.
[C#], 361 355 bytes
using System;class P{static void Main(){Func<string,int>F=f=>"14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196".IndexOf(f)+1;Action<int>w=Console.WriteLine;w(F("1"));w(F("65"));w(F("93993"));w(F("3"));}}

Formatted version:
using System;

class P
{
    static void Main()
    {
        Func<string,int>F=f=>"14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196".IndexOf(f)+1;
        Action<int>w=Console.WriteLine;
        w(F("1"));
        w(F("65"));
        w(F("93993"));
        w(F("3"));
    }
}

Ideone!
NB.I miscounted the first version. It was 361 bytes, not 363 bytes.
[C#], tio version 218 bytes
f=>"14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196".IndexOf(f)+1

Try it online!

You don't need to include the test cases in your code, and you can just use a lambda (anonymous) function instead of a full program

Hyarus suggested using System;f=>"14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196".IndexOf(f)+1; as an edit.

I'm new here and I thought I must include a full program including the test case. It seems people are using tio.run for demonstration instead of ideone. I see that tio.run divide the code into parts.

Ruby, 37 35 bytes
p"#{BigMath::PI 200}"[3..-3]=~/#$_/

Try it online!
Nothing special, just showcasing the built-in library. Output is 0-indexed.
The Pi string is formatted as 0.31415...e1, so we need to strip off the first 3 chars. The e1 part in the end doesn't really do any harm, but it is stripped off too, as we need to provide a range end (or slice length) value anyway.

short AND readable!

Haskell, 230 bytes
Using laziness to find the number anywhere in the infinite digits of pi, not just in the first 200 digits. Oh yeah, and it returns you every (infinitely many?) instance(s) of the number, not just the first one.
p=g(1,0,1,1,3,3)where g(q,r,t,k,n,l)=if 4*q+r-t<n*t then n:g(10*q,10*(r-n*t),t,k,div(10*(3*q+r))t-10*n,l) else g(q*k,(2*q+r)*l,t*l,k+1,div(q*(7*k+2)+r*l)(t*l),l+2)
z n=[(i,take n$drop i p)|i<-[1..]]
f l=[n|(n,m)<-z$length l,m==l]

Examples from the challenge
>  take 10 $ f [1]
[1,3,37,40,49,68,94,95,103,110]
>  take 10 $ f [6,5]
[7,108,212,239,378,410,514,672,870,1013]
>  take 1 $ f [9,3,9,9,3]
[42]
>  take 10 $ f [3]
[9,15,17,24,25,27,43,46,64,86]

Credits
'p' is the infinite stream of pi digits, taken from https://rosettacode.org/wiki/Pi#Haskell
> take 20 p
[3,1,4,1,5,9,2,6,5,3,5,8,9,7,9,3,2,3,8,4]

I guess you already know this, but you only need to output the first number in your sequence...

Just thought I'd embrace the infinite-ness :D

Jelly, 24 bytes
ȷ*
ȷR×¢:Ḥ‘$ƲU×:¢+¢ʋ/ḤṾḊw

Try it online!
Use a Machin-like formula, specifically 1/4 pi == tan-1(1/2) + tan-1(1/3).
Use the formula pi/2 == 1 + 1/3 × (1 + 2/5 × (1 + 3/7 × (1 + 4/9 × ( ... ))))

Is there a way to get digits from ØP in M?

@dylnan Somewhat, but M is not Jelly.

I know they're different. Can't believe I didn't think of floor. Mind if I use that to post as answer in M?

Nevermind. Doesn't work above 104 digits...

AWK -M , 131 119 117 bytes
Uses -M flag for arbitrary precision calculations.
Added p=k=0 (5 bytes) to the TIO link to allow multi-line input
{CONVFMT="%.999f";PREC=1e3;for(p=k=0;k<1e3;)p+=(4/(8*k+1)-2/(8*k+4)-1/(8*k+5)-1/(8*k+6))/16^k++;$0=$1==3?9:index(p,$1)-2}1

Try it online!
Explanation:
{CONVFMT="%.999f";  # Allows 999 decimal digits to be used when numbers are convert to strings
PREC=1e3;           # Digits of precision to use for calculations
for(;k<1e3;)p+=(4/(8*k+1)-2/(8*k+4)-1/(8*k+5)-1/(8*k+6))/16^k++; # The most concise numerical calculation I could find. It doesn't converge  extremely rapidly, but it seems to work OK
$0=$1==3?9:index(p,$1)-2}  # Replace input line with either 9 or index-2
                           # since indices will either be 1 (meaning 3 was input) or >= 3
1                   # Print the "new" input line

My first attempt used sprintf to get the decimals.  Using CONVFMT is definitely cleaner.

No need to use the flag: meta consensus is to consider this a language distinct from AWK, "AWK with -M flag"

Good to know. I guess I should spend more time on meta... with my loads of free time. :)

Python 2 239 238 229 214 bytes
-9 bytes due to @primo
from bigfloat import*;a=s=n=10**10**5;b=k=0
while a:k+=1;a*=k*(k*(108-72*k)-46)+5;a/=k**3*(640320**3/24);s+=a;b+=k*a
with precision(10**7):print`(426880*sqrt(10005*n)*n)/(13591409*s+545140134*b)`.find(input())-16

Uses the Chudnovsky-Ramanujan algorithm to find the first 1 million digits 50000 digits of π (change 10**10**5 to 10**10**6 for more, but it takes ages to run) and then searches them for the desired string.

I tried to confirm the result but it doesn't seem to terminate (n=10**10**5 takes about 10s).

@primo I never said it was fast! 10**10**6 takes about 7 minutes on my machine.. To be fair, 10**10**5 gives the first 50000 digits, so I guess it's not that bad either :)

@primo I've changed the arbitrary precision library to bigfloat, it runs much quicker now.

It's much faster now, I was going to suggest switching to gmpy2, but bigfloat saves a dozen or so bytes. The assignment of k can be merged with k=b=0 if you move k+=1 to the start of the iteration. -(6*k-5)*(2*k-1)*(6*k-1) can be written more succinctly as k*(k*(108-72*k)-46)+5. If you declare Python 2, the // integer divisions can be replaced by /, and also parentheses aren't necessary for print. Space can also be removed in import*. Only validates to 50000 digits, btw.

The n in sqrt(10005*n) seems to be the problem; it's moving the decimal point to 50000th place. In case you're interested, here's my own Chudnovsky implementation: Try it online!

@primo Thanks! I did try gmpy2, but like you say, the program was 2 bytes longer. The 301000 figure was when using gmpy2, but since I'm using bigfloat, I'll fix that.

Javascript 217 bytes (200 hardcoded)
a=>"14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196".search(a)+1

PHP, 27 bytes
Not a very serieus answer, it requires a change in the php.ini settings as pi() defaults to 14 digits, not 200, but for once the PHP solution is fairly elegant:
<?=strpos(pi(),$_GET[n])-1;

I don't think this will actually work. the precision tag in php.ini only alters the display precision, and doesn't actually increase the precision of defined constants. witness

Julia 0.6, 53 bytes
setprecision(9^6)
x->searchindex("$(big(π))","$x",3)

Set the precision for BigFloats high enough, then convert pi to a string and search. Precision of 9^6 handles 159980 digits.
Try it online!

J, 25 Bytes
{.I.(}.":<.@o.10x^999)E.~

Try it online!
0-Indexed
Takes input as a string, +2 Bytes (":) if that's not allowed.
Explanation eventually.

Perl 5 with -MMath::BigFloat+bpi and -n, 20 bytes
bpi($>)=~/.$_/;say@-

Try it online!
I'm not sure where usage of $> stands, since it's the EFFECTIVE_USER_ID which is not portable, but on TIO this is 1000 and satisfies our requirement, for -1 byte vs. 200.

Husk, 5 bytes
€tİπd

Try it online!
€        The 1-based index as a substring of
    d    the decimal digits of
         the input
  İπ     in the infinite list of digits of pi
 t       after the radix point.

lol

@Razetime lmao, even

JavaScript (Node.js) (ES2020), 75 bytes
n=>`${eval(`for(a=c=2n*10n**300n,d=1n;a*=d;)c+=a/=d+++d`)}`.search("."+n)+1

Try it online!
Uses the formula I've used in another Pi-related challenge. search("."+n) is needed to drop the leading 3. Change 300 to a higher number gives more precision.

source: Stack Exchange

license: Creative Commons - Attribution Share-Alike - https://creativecommons.org/licenses/by-sa/4.0/

all_licenses: Creative Commons - Attribution Share-Alike - https://creativecommons.org/licenses/by-sa/3.0/

sort: votes


text:
ASCII-art to numbers
Inspired by Digits in their lanes
Input:
An ASCII-art of width ≤ 11, consisting of spaces and #. (You can choose any two distinct characters instead.) Example:
     #
    ###
     #
     #
    # #
   #   #
  #     #
 #  ###  #
#   ###   #
###########
#         #
#         #
#   ###   #
#   ###   #
#   ###   #
###########

Output:
A list of integers, with one element for each line of the input.
If you put a hash in each decimal digit's lane, including the minus sign, in
the order -0123456789. Duplicated digits are allowed, but ignored. The order of the digits in the output is not important.
Possible outputs for the above input include:
[ 4, 345, 4, 4, 35, 26, 17, 34580, -3459, -9876543210, -9, -9, -3459, -3459, -3459, -1234567890 ]
[ 4444444, 5345354354, 4, 44, 535, 2666, 71, 85430, -3495939495, -93678132645160234, -99, -99999, -934539, -935439, -9534, -9876543210 ]

Note that you have to distinguish between 0 and -0. If your output format doesn't support that, you can say there is a special value for -0 (e.g. None).
Leading zeros
If a number is 0 (or -0), the zero is always counted.
Else, you have to move the zero after the first digit (not necessarily next to it): For example, -09 stands for - and 9, so you have to output -90 instead. So, even if you output the string "-09" where -, 0 and 9 are #, that is not right.

In your output, leading zeroes are not counted (that is, the output is the same as if those leading zeroes are removed). This does also include zeroes directly after the minus signs.

Here are some examples for clarification:
-0123456789    OK           not OK
##          -> -0
###         -> -10          -01
##        # -> -90          -09
 ##         -> 10           01
  #         -> 01           10

This does also apply when you output a string!

General rules

You can assume that in every line, at least one of 0-9 is a # (not empty or only -)
You can submit a program or function
Choose any reasonable input/output format (eg. list of lines, list of characters, etc.)

Scoring

Your score is the number of bytes in your code.
Lowest score wins.

Loopholes

Standard loopholes are forbidden

Examples
Note that there is an infinite number of correct outputs for every input, here,
only one is mentioned. If you need to verify an output, you can usually use an
answer to
Digits in their lanes
and input your output. Then compare it's output with the original input.
     #         4
    ###        345
     #         4
     #         4
    # #        35
   #   #       26
  #     #      17
 #  ###  #     83450
#   ###   # -> -9534
###########    -9876543210
#         #    -9
#         #    -9
#   ###   #    -3459
#   ###   #    -3459
#   ###   #    -3459
###########    -1234567890

 #########     123456780
#         #    -9
#  ##  ## #    -23679
# #   #   #    -159
# #   # # #    -1579
#  ##  ## # -> -23679
#         #    -9
 ##### ###     12346780
     ##        45
     #         4

##   ##  ##    -45890
# # #   #      -137
##  #   #   -> -370
#   #   # #    -379
#    ##  ##    -4589

## ## ## ##    -2356890
#  #     ## -> -289
#  #           -2

##             -0
 ##            10
  ##           12
   ##          23
    ##      -> 34
     ##        45
      ##       56
       ##      67
        ##     78
         ##    89

Why the minus sign?

@fəˈnɛtɪk Well .. Digits in their lanes includes it ...

Is -09 allowed when -9 is required?

@l4m2 Yes, it is

Is a list of digits allowed in place of a list of characters for input?

@dylnan Yes, it is

Can we output a list of strings (not lines like Digits in their lanes, just strings containing the -s and the digits)?

@EriktheOutgolfer Sure, but the strings are intepreted as numbers, so -09 is still only - and 9. And something like 102-3 is not a valid number, therefor no valid output.

@wastl -09 isn't the same as -9 though, that's why I'm using strings.

Stax, 11 bytes
ñ╬ü+U☻T→╡aN

Run and debug it
Unpacked, ungolfed, and commented, it looks like this.
m           for each line of input, run the rest and implicitly output
  |(        rotate string left once
  :A        get indices of maxima (indices of '#')
  Vd'-+s    push "0123456789-" under the top of the stack
  @         get characters at indices
  r         reverse string; puts '-' at the front
            output is implicit

Run this one

Jelly, 13 bytes
...turns out it's slightly different to Dylnan's method, I thought they just beat me to it
ṙ€1T€ịØD;”-¤U

A monadic link accepting a list of lists of 1s and 0s which returns a list of lists of characters the output "numbers".
Try it online!
How?
ṙ€1T€ịØD;”-¤U - Link: list of lists of integers (in {0,1})
ṙ€1           - rotate €ach list left by one
   T€         - get the truthy (1-based) indices of €ach
           ¤  - nilad followed by link(s) as a nilad:
      ØD      -   decimal digit characters = "0123456789"
         ”-   -   literal '-' character
        ;     -   concatenate
     ị        - index into (vectorises)
            U - upend (reverses each resulting list of characters)

OP commented on my answer, verbatim, that "No, this is not allowed (Specs: So, even if you output the string "-09" where -, 0 and 9 are #, that is not right)". I'm not sure if this answer is invalid too because of this.

This never outputs -09

Yes, this one is correct.

Perl 5 -lp, 35 bytes
Uses # and ;
#!/usr/bin/perl -lp
s/./"$&@--1"/eeg;s/-1/-/;s;0(.);$+0

Try it online!

Specs: So, even if you output the string "-09" where -, 0 and 9 are #, that is not right.

@wastl I made the minimal fix to conform to the spec. I'll think about regolfing later

05AB1E, 18 17 bytes
Currently 3 bytes to make sure the number doesn't start with zero. Looking for a shorter way.
vžh'-ìyƶ0K<ΣΘ}èJˆ

Try it online!
or with ascii-art input
Uses 1 instead of # and 0 instead of space.

Fails for line 9 (leading zeroes do not count!)

Maybe output the numbers reverse?

@wastl: Missed that requirement. Fixed now.

Now, it seems to fail for asymmetrical input (I have no idea of 05AB1E, but probably you are reversing the input?)

@wastl: Yeah, messed up the golf. I've gone back to the 18-byter again :(

JavaScript (ES7), 60 55 bytes
Takes input as an array of strings with 0 instead of #. Returns an array of strings.
a=>a.map(r=>('-'+2**67).replace(/./g,c=>[c[r[++c|0]]]))

Try it online!
Commented
a =>                    // given the input array a[]
  a.map(r =>            // for each row r of a[]
    ('-' + 2**67)       //   generate the string '-147573952589676410000'
    .replace(/./g, c => //   replace each character c of r with either c or ''
      [                 //     wrap the result into [] so that undefined is coerced to ''
       c[               //     read c['0'] (gives c) or c[' '] (gives undefined)
         r[             //     read r[] --> gives '0' or ' '
           ++c | 0]]]   //     gives (NaN | 0) = 0 if c is '-', or (c + 1) if c is a digit
    )                   //   end of replace()
  )                     // end of map()

Your code seems to work, but if you scroll down the test cases, you can see that your last one is longer, and there is an additional one

@wastl Oops... Fixed :)

Java 10, 176 136 bytes
c->{int l=c.length,i=0,j;var o=new String[l];for(String s;i<l;o[i]=c[i++][0]<8?"-"+s:s)for(s="",j=10;j>0;)s+=c[i][j--]<8?j:"";return o;}

Returns an array of Strings. Uses the BEL character instead of #.
Try it online here.
Thanks to Kevin Cruijssen for golfing 40 bytes.
Ungolfed version:
c -> { // lambda taking a char[][] as argument
    int l = c.length, // the number of lines
    i = 0, //used for iterating over all lines
    j; // used for iterating over each line
    var o = new String[l]; // output array
    for(String s; // the output for the current line
        i < l; // iterate over all lines
        o[i] = c[i++][0] < 8 ? "-"+s : s) // add a minus if necessary
        for(s = "", j = 10; j>0; ) // to avoid leading zeroes, we step through the line backwards
            s += c[i][j--] < 8 ? j : ""; // append the next digit, if applicable
    }
    return o; // return the output array
}

You can golf 10 bytes like this: c->{int l=c.length,i=0,j;var o=new Long[l];for(;i<l;o[i++]=s.equals("-0")?null:new Long(s)){var s="";for(j=10;j>0;)s+=c[i][j--]<8?j:"";s=c[i][0]<8?"-"+s:s;}return o;}

136 bytes if you output a String-array instead: c->{int l=c.length,i=0,j;var o=new String[l];for(var s="";i<l;o[i]=c[i++][0]<8?"-"+s:s)for(s="",j=10;j>0;)s+=c[i][j--]<8?j:"";return o;} :)

@KevinCruijssen very nice, thank you :) i missed that the challenge was changed to allow String output

131 bytes

Jelly, 20 14 bytes
ØD”-;ẋ"Ð€ṙ€1Ṛ€

Try it online!
Function submission. Takes a list of lines as input. Characters are 1 for on and 0 for off.
Explanation
ØD”-;ẋ"Ð€ṙ€1Ṛ€
ØD               Digits 0-9 as characters
  ”-             Character literal -
    ;            Concatenate -> -0123456789
                 Turn each 0 and 1 from the input (characters) into an integer.
       Ð€        For each list of integers 0 and 1 corresponding to the list of lines in the input...
      "          Zip the characters -0123456789 with the 0s and 1s.
     ẋ           Include each of the characters if paired with a 1, not if paired with a 0.
                 Characters that get included turn into ['3'] (3 as an example)
                 Those that don't turn into []. This is important for the next step.
          €      For each of the lists of [character]s and []s.
         ṙ 1     rotate it by 1. This moves the ['-'] or [] in place of ['-'] to the end of the line.
            Ṛ€   Reverse €ach line. Brings the ['-'] to the front and the leading ['0'] if present to the end.

Oh, very similar to mine, I did not notice. I'm questioning the need for V€€ by the way - it says "reasonable" which is a little subjective... (see my deleted post)

Ṛ€ may be replaced by U :)

@JonathanAllan Hmm I'll consider taking V€€ out. I'll ask OP about that. Unfortunately since each character is wrapped in a list U skips past the list of lines level and doesn't do anything here.

List of numbers is OK (05AB1E answer uses it too)

Ah our methods differ - I used the "truthy" atom: ṙ€1T€ịØD;”-¤U

@JonathanAllan Yeah, beat me by 1! I took out V€€ and somehow it still works with character input. I guess ẋ can handle characters/strings for the right argument.

It casts its right argument to an int, so it works for a digit character on the right (it also vectorises so a "string" (list of characters) on the right repeats by the int of each character in turn - e.g. ['s']...ẋ...['2','3'] yields [['s','s'],['s','s','s']])

APL+WIN, 58 bytes
Prompts for a character matrix:
(⊂[2]z[;1],⌽0 1↓z←' -0123456789'[1+n×(⍴n←⎕='#')⍴⍳11])~¨' '

Outputs digits in reverse order to cope with leading zeros.

Python 2, 74 bytes
lambda s:[''.join(`i-1`[0]for i in[0]+range(10,0,-1)if' '<l[i])for l in s]

Try it online!

Perl 6, 54 bytes
{.map:{(.ords.grep(:k,*>32)X-1).sort(1/*)>>.ord.chrs}}

Try it online!
Takes a list of lines. Explanation:
{
    .map:{                     # For each line.
        (.ords.grep(:k,*>32)   # Find non-whitespace indices.
         X- 1)                 # Decrement each, range is now -1..9.
        .sort(1/*)             # Sort by reciprocal, moving 0s to the end.
        >>.ord.chrs            # Join first characters.
    }
}

You can save a byte if you use a lower character instead of space (e.g. \t)

R, 83 bytes
for(i in gregexpr("#",readLines()))cat(sub(99,0,sort(c("-",99,1:9)[i])),'
',sep="")

Try it online!
A nasty 83 bytes; would have been so much shorter (and simpler of a challenge, I suppose) to not have to move the 0 to the end. Ah well. Uses 99 in place of 0 to utilize sort to move 0 to the end, but that comes at the cost of having to use sub.

C# (Visual C# Compiler), 123 bytes
using System.Linq;l=>l.Select(k=>{var c=k[0]!=' '?"-":"";for(int a=k.Length;a>1;a--)if(k[a-1]!=' ')c+=$"{a-2}";return c;});

Try it online!

Retina 0.8.2, 34 bytes
(.)(.*)
$2$1
-(?=.)
$.%`

%O^$`.

Try it online! Takes input using -s instead of #s, but the linked header includes the substitution. Explanation:
(.)(.*)
$2$1

Move the first character of each line to the end.
-(?=.)
$.%`

Replace each - not at the end of a line with its column number.

Delete the spaces.
%O^$`.

Reverse each line.

license: Creative Commons - Attribution Share-Alike - https://creativecommons.org/licenses/by-sa/3.0/


text:
(A → B) → (¬B → ¬A)
Well I think it is about time we have another proof-golf question.
This time we are going to prove the well known logical truth
\$(A \rightarrow B) \rightarrow (\neg B \rightarrow \neg A)\$
To do this we will use Łukasiewicz's third Axiom Schema, an incredibly elegant set of three axioms that are complete over propositional logic.
Here is how it works:
Axioms
The Łukasiewicz system has three axioms. They are:
\$\phi\rightarrow(\psi\rightarrow\phi)\$
\$(\phi\rightarrow(\psi\rightarrow\chi))\rightarrow((\phi\rightarrow\psi)\rightarrow(\phi\rightarrow\chi))\$
\$(\neg\phi\rightarrow\neg\psi)\rightarrow(\psi\rightarrow\phi)\$
The axioms are universal truths regardless of what we choose for \$\phi\$, \$\psi\$ and \$\chi\$.  At any point in the proof we can introduce one of these axioms.  When we introduce an axiom you replace each case of \$\phi\$, \$\psi\$ and \$\chi\$, with a "complex expression".  A complex expression is any expression made from Atoms, (represented by the letters \$A\$-\$Z\$), and the operators implies (\$\rightarrow\$) and not (\$\neg\$).
For example if I wanted to introduce the first axiom (L.S.1) I could introduce
\$A\rightarrow(B\rightarrow A)\$
or
\$(A\rightarrow A)\rightarrow(\neg D\rightarrow(A\rightarrow A))\$
In the first case \$\phi\$ was \$A\$ and \$\psi\$ was \$B\$, while in the second case both were more involved expressions.  \$\phi\$ was \$(A\rightarrow A)\$ and \$\psi\$ was \$\neg D\$.
What substitutions you choose to use will be dependent on what you need in the proof at the moment.
Modus Ponens
Now that we can introduce statements we need to relate them together to make new statements.  The way that this is done in Łukasiewicz's Axiom Schema (L.S) is with Modus Ponens.  Modus Ponens allows us to take two statements of the form
\$\phi\$
\$\phi\rightarrow \psi\$
and instantiate a new statement
\$\psi\$
Just like with our Axioms \$\phi\$ and \$\psi\$ can stand in for any arbitrary statement.
The two statements can be anywhere in the proof, they don't have to be next to each other or any special order.
Task
Your task will be to prove the law of contrapositives.  This is the statement
\$(A\rightarrow B)\rightarrow(\neg B\rightarrow\neg A)\$
Now you might notice that this is rather familiar, it is an instantiation of the reverse of our third axiom
\$(\neg\phi\rightarrow\neg\psi)\rightarrow(\psi\rightarrow\phi)\$
However this is no trivial feat.
Scoring
Scoring for this challenge is pretty simple, each time you instantiate an axiom counts as a point and each use of modus ponens counts as a point.  This is essentially the number of lines in your proof.  The goal should be to minimize your score (make it as low as possible).
Example Proof
Ok now lets use this to construct a small proof.  We will prove \$A\rightarrow A\$.
Sometimes it is best to work backwards since we know where we want to be we can figure how we might get there.  In this case since we want to end with \$A\rightarrow A\$ and this is not one of our axioms we know the last step must be modus ponens.  Thus the end of our proof will look like
φ
φ → (A → A)
A → A       M.P.

TeX
Where \$\phi\$ is an expression we don't yet know the value of.  Now we will focus on \$\phi\rightarrow(A\rightarrow A)\$.  This can be introduced either by modus ponens or L.S.3.  L.S.3 requires us to prove \$(\neg A\rightarrow\neg A)\$ which seems just as hard as \$(A\rightarrow A)\$, so we will go with modus ponens.  So now our proof looks like
φ
ψ
ψ → (φ → (A → A))
φ → (A → A)        M.P.
A → A              M.P.

TeX
Now \$\psi\rightarrow(\phi\rightarrow(A\rightarrow A))\$ looks a lot like our second axiom L.S.2 so we will fill it in as L.S.2
A → χ
A → (χ → A)
(A → (χ → A)) → ((A → χ) → (A → A)) L.S.2
(A → χ) → (A → A)                   M.P.
A → A                               M.P.

TeX
Now our second statement \$(A\rightarrow(\chi\rightarrow A))\$ can pretty clearly be constructed from L.S.1 so we will fill that in as such
A → χ
A → (χ → A)                         L.S.1
(A → (χ → A)) → ((A → χ) → (A → A)) L.S.2
(A → χ) → (A → A)                   M.P.
A → A                               M.P.

TeX
Now we just need to find a \$\chi\$ such that we can prove \$A\rightarrow\chi\$.  This can very easily be done with L.S.1 so we will try that
A → (ω → A)                                     L.S.1
A → ((ω → A) → A)                               L.S.1
(A → ((ω → A) → A)) → ((A → (ω → A)) → (A → A)) L.S.2
(A → (ω → A)) → (A → A)                         M.P.
A → A                                           M.P.

TeX
Now since all of our steps our justified we can fill in \$\omega\$, as any statement we want and the proof will be valid.  We could choose \$A\$ but I will choose \$B\$ so that it is clear that it doesn't need to be \$A\$.
A → (B → A)                                     L.S.1
A → ((B → A) → A)                               L.S.1
(A → ((B → A) → A)) → ((A → (B → A)) → (A → A)) L.S.2
(A → (B → A)) → (A → A)                         M.P.
A → A                                           M.P.

TeX
Try it online!
And that is a proof.
Resources
Verification program
Here is a Prolog program you can use to verify that your proof is in fact valid.  Each step should be placed on its own line. -> should be used for implies and - should be used for not, atoms can be represented by any string of alphabetic characters.
Metamath
Metamath uses the Łukasiewicz system for its proofs in propositional calculus, so you may want to poke around there a bit.  They also have a proof of the theorem this challenge asks for which can be found here.  There is an explanation here of how to read the proofs.
The Incredible Proof Machine
@Antony made me aware of a tool called The Incredible Proof machine which allows you to construct proofs in a number of systems using a nice graphical proof system.  If you scroll down you will find they support the Łukasiewicz system.  So if you are a more visual oriented person you can work on your proof there.  Your score will be the number of blocks used minus 1.

Hold on, let me go fetch my Discrete Math notebook...

Is it possible that I studied this during Math undergraduate 20 years ago?  If so, I sadly have no recollection :(  Looks like an interesting challenge for those with the expertise to take it on...

@DigitalTrauma I'm a undergrad now and this was a homework assignment I had (minus the golf part), so its very possible that you may have studied it.  I encourage you to give it a try even if you lack "expertise", I think this challenge is approachable even for people who's background is mostly in programming.

Can we use the Deduction Theorem? It's unclear to me how to solve this without using it. It essentially follows from the first axiom, which may be worded "If we have a derivation of Y from a premise X then we are allowed to infer X→Y, provided that the premise X is discharged." Deduction makes things a lot easier, because then you can use assumptions to deduce implications.

@mbomb007 You cannot use the Deduction Theorem, and since the Łukasiewicz system is complete you do not need to use it.

Well at least you didn't limit the axioms to a single, universal schema: ((P → Q) → R) → ((R → P) → (S → P))

The Incredible Proof Machine is all drag and drop and supports Łukasiewicz's.  Scroll almost to the bottom and look for "Hilbert system".  For example here is the proof @user56656 gave that A→A

Can we replace ~~A with A?

@Acccumulation No you cannot,  you can prove that ~~A -> A and use that but you cannot just substitute A for ~~A.

@user56656 Yeah, otherwise the proof would be trivial. That's basically what I've been working to prove. Most of my proofs would use deduction, though. Metamath has the way to use modus ponens to prove deduction, so I think in the end I'll have to use that and expand it in every occurrence if I can't work without it.

Retina script to add line numbers and tabs to the output of the Prolog program.

Wouldn't it be more fun to ask for code to search for short proofs?

@Anush I don't know. Probably not, but that's not this challenge.

Can this model prove (A->(B->C))->(B->(A->C))?

@l4m2 The model is complete and consistent.  It can prove any true statement within propositional logic.  And since the statement you gave is true it can be proven.

Proudly gave the 42th upvote. Shame I missed this challenge. Btw., 59 steps, as by the community wiki answer, is still the smallest known proof for that theorem in this Hilbert system. (See *2.16 in pmproofs.txt of the Metamath Solitaire project.)

88 82 77 72 steps
Thanks to H.PWiz for better combinator conversions that saved 10 steps!
Explanation
You might be familiar with the Curry–Howard correspondence, in which theorems correspond to types and proofs correspond to programs of those types.  The first two axioms in the Łukasiewicz system are actually the K and S combinators, and it’s well known that we can translate lambda calculus expressions into the SK combinatory expressions.
So let’s write down some expressions corresponding to our axioms (the following is valid Haskell syntax, which is convenient because we can quite literally check our proofs using the Haskell compiler):
data Not φ

k :: φ -> (ψ -> φ)
k x _ = x

s :: (φ -> (ψ -> χ)) -> ((φ -> ψ) -> (φ -> χ))
s x y z = x z (y z)

c :: (Not φ -> Not ψ) -> (ψ -> φ)
c = error "non-computational axiom"

Then we can write a proof of the desired statement as a program in terms of c (this part takes a bit of cleverness, but it’s much easier to write this than an 72-line axiomatic proof):
pf :: (a -> b) -> (Not b -> Not a)
pf x y = c (\z -> c (\_ -> y) (x (c (c (\_ -> z)) x))) k

and convert it into an SK combinatory expression:
pf' :: (a -> b) -> (Not b -> Not a)
pf' =
  s (k (s (k (s c (k k)))))
    (s (k (s (s (k s) (s (k k) (s (k c) k)))))
       (s (k k) (s (k (s s (s (s (k c) (s (k c) k))))) k)))

The 17 k, 16 s, and 4 c combinators above correspond to the 16 LS1, 16 LS2, and 4 LS3 invocations in the proof below, and the 38 applications of a function to a value above correspond to the 38 MP invocations below.
Why only 16 LS1 invocations?  It turns out one of the k combinators above has a free type variable, and instantiating it carefully turns it into a duplicate of another one that has already been derived.
The proof

(A → B) → (¬¬A → (A → B)) LS1
¬¬A → (¬¬(A → B) → ¬¬A) LS1
(¬¬(A → B) → ¬¬A) → (¬A → ¬(A → B)) LS3
((¬¬(A → B) → ¬¬A) → (¬A → ¬(A → B))) → (¬¬A → ((¬¬(A → B) → ¬¬A) → (¬A → ¬(A → B)))) LS1
¬¬A → ((¬¬(A → B) → ¬¬A) → (¬A → ¬(A → B))) MP 4,3
(¬¬A → ((¬¬(A → B) → ¬¬A) → (¬A → ¬(A → B)))) → ((¬¬A → (¬¬(A → B) → ¬¬A)) → (¬¬A → (¬A → ¬(A → B)))) LS2
(¬¬A → (¬¬(A → B) → ¬¬A)) → (¬¬A → (¬A → ¬(A → B))) MP 6,5
¬¬A → (¬A → ¬(A → B)) MP 7,2
(¬A → ¬(A → B)) → ((A → B) → A) LS3
((¬A → ¬(A → B)) → ((A → B) → A)) → (¬¬A → ((¬A → ¬(A → B)) → ((A → B) → A))) LS1
¬¬A → ((¬A → ¬(A → B)) → ((A → B) → A)) MP 10,9
(¬¬A → ((¬A → ¬(A → B)) → ((A → B) → A))) → ((¬¬A → (¬A → ¬(A → B))) → (¬¬A → ((A → B) → A))) LS2
(¬¬A → (¬A → ¬(A → B))) → (¬¬A → ((A → B) → A)) MP 12,11
¬¬A → ((A → B) → A) MP 13,8
(¬¬A → ((A → B) → A)) → ((¬¬A → (A → B)) → (¬¬A → A)) LS2
(¬¬A → (A → B)) → (¬¬A → A) MP 15,14
(¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B)) LS2
((¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B))) → (((¬¬A → (A → B)) → (¬¬A → A)) → ((¬¬A → (A → B)) → (¬¬A → B))) LS2
((¬¬A → (A → B)) → (¬¬A → A)) → ((¬¬A → (A → B)) → (¬¬A → B)) MP 18,17
(¬¬A → (A → B)) → (¬¬A → B) MP 19,16
((¬¬A → (A → B)) → (¬¬A → B)) → ((A → B) → ((¬¬A → (A → B)) → (¬¬A → B))) LS1
(A → B) → ((¬¬A → (A → B)) → (¬¬A → B)) MP 21,20
((A → B) → ((¬¬A → (A → B)) → (¬¬A → B))) → (((A → B) → (¬¬A → (A → B))) → ((A → B) → (¬¬A → B))) LS2
((A → B) → (¬¬A → (A → B))) → ((A → B) → (¬¬A → B)) MP 23,22
(A → B) → (¬¬A → B) MP 24,1
(¬¬A → B) → (¬B → (¬¬A → B)) LS1
((¬¬A → B) → (¬B → (¬¬A → B))) → ((A → B) → ((¬¬A → B) → (¬B → (¬¬A → B)))) LS1
(A → B) → ((¬¬A → B) → (¬B → (¬¬A → B))) MP 27,26
((A → B) → ((¬¬A → B) → (¬B → (¬¬A → B)))) → (((A → B) → (¬¬A → B)) → ((A → B) → (¬B → (¬¬A → B)))) LS2
((A → B) → (¬¬A → B)) → ((A → B) → (¬B → (¬¬A → B))) MP 29,28
(A → B) → (¬B → (¬¬A → B)) MP 30,25
¬B → (¬¬(¬¬A → (¬¬(A → B) → ¬¬A)) → ¬B) LS1
(¬¬(¬¬A → (¬¬(A → B) → ¬¬A)) → ¬B) → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) LS3
((¬¬(¬¬A → (¬¬(A → B) → ¬¬A)) → ¬B) → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → ((¬¬(¬¬A → (¬¬(A → B) → ¬¬A)) → ¬B) → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) LS1
¬B → ((¬¬(¬¬A → (¬¬(A → B) → ¬¬A)) → ¬B) → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) MP 34,33
(¬B → ((¬¬(¬¬A → (¬¬(A → B) → ¬¬A)) → ¬B) → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → ((¬B → (¬¬(¬¬A → (¬¬(A → B) → ¬¬A)) → ¬B)) → (¬B → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) LS2
(¬B → (¬¬(¬¬A → (¬¬(A → B) → ¬¬A)) → ¬B)) → (¬B → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) MP 36,35
¬B → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) MP 37,32
(B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) LS1
((B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → (¬B → ((B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) LS1
¬B → ((B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) MP 40,39
(¬B → ((B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) → ((¬B → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) LS2
(¬B → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) MP 42,41
¬B → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) MP 43,38
(¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) LS2
((¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → (¬B → ((¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) LS1
¬B → ((¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) MP 46,45
(¬B → ((¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) → ((¬B → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → (¬B → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) LS2
(¬B → (¬¬A → (B → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → (¬B → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) MP 48,47
¬B → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) MP 49,44
(¬B → ((¬¬A → B) → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → ((¬B → (¬¬A → B)) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) LS2
(¬B → (¬¬A → B)) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) MP 51,50
((¬B → (¬¬A → B)) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → ((A → B) → ((¬B → (¬¬A → B)) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) LS1
(A → B) → ((¬B → (¬¬A → B)) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) MP 53,52
((A → B) → ((¬B → (¬¬A → B)) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) → (((A → B) → (¬B → (¬¬A → B))) → ((A → B) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))))) LS2
((A → B) → (¬B → (¬¬A → B))) → ((A → B) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) MP 55,54
(A → B) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) MP 56,31
(¬¬A → (¬¬(A → B) → ¬¬A)) → ((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (¬¬(A → B) → ¬¬A))) LS1
(¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (¬¬(A → B) → ¬¬A)) MP 58,2
(¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ((¬¬A → (¬¬(A → B) → ¬¬A)) → ¬A) LS3
((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ((¬¬A → (¬¬(A → B) → ¬¬A)) → ¬A)) → (((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (¬¬(A → B) → ¬¬A))) → ((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ¬A)) LS2
((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → (¬¬A → (¬¬(A → B) → ¬¬A))) → ((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ¬A) MP 61,60
(¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ¬A MP 62,59
((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ¬A) → (¬B → ((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ¬A)) LS1
¬B → ((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ¬A) MP 64,63
(¬B → ((¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))) → ¬A)) → ((¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → ¬A)) LS2
(¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → ¬A) MP 66,65
((¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → ¬A)) → ((A → B) → ((¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → ¬A))) LS1
(A → B) → ((¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → ¬A)) MP 68,67
((A → B) → ((¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A)))) → (¬B → ¬A))) → (((A → B) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → ((A → B) → (¬B → ¬A))) LS2
((A → B) → (¬B → (¬¬A → ¬(¬¬A → (¬¬(A → B) → ¬¬A))))) → ((A → B) → (¬B → ¬A)) MP 70,69
(A → B) → (¬B → ¬A) MP 71,57

Try it online!

Wow, this is amazing.

I can't tell if it's shorter in steps, and have to go right now. But I got s(s(k s)(s(k(s(k c)))(s(k(s(s(k s)(s(k k)(s(k c)k)))))(s(k k)(s(k(s s(s(s(k c)(s(k c)k)))))k)))))k  which is similar to yours but with a slightly shorter ending

@H.PWiz Neat, that actually corresponds to a slightly different proof program. Updated.

How about s(k(s(k(s c(k s)))))(s(k(s(s(k s)(s(k k)(s(k c)k)))))(s(k k)(s(k(s s(s(s(k c)(s(k c)k)))))k)))?

@H.PWiz That’s good for another −5 along with the free type variable trick.

91 Steps
Full Proof:
1. (A → B) → (¬¬A → (A → B)) LS1
2. (¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B)) LS2
3. ((¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B))) → ((A → B) → ((¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B)))) LS1
4. (A → B) → ((¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B))) MP 3,2
5. ((A → B) → ((¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B)))) → (((A → B) → (¬¬A → (A → B))) → ((A → B) → ((¬¬A → A) → (¬¬A → B)))) LS2
6. ((A → B) → (¬¬A → (A → B))) → ((A → B) → ((¬¬A → A) → (¬¬A → B))) MP 5,4
7. (A → B) → ((¬¬A → A) → (¬¬A → B)) MP 6,1
8. ¬A → (¬¬(B → (¬A → A)) → ¬A) LS1
9. (¬¬(B → (¬A → A)) → ¬A) → (A → ¬(B → (¬A → A))) LS3
10. ((¬¬(B → (¬A → A)) → ¬A) → (A → ¬(B → (¬A → A)))) → (¬A → ((¬¬(B → (¬A → A)) → ¬A) → (A → ¬(B → (¬A → A))))) LS1
11. ¬A → ((¬¬(B → (¬A → A)) → ¬A) → (A → ¬(B → (¬A → A)))) MP 10,9
12. (¬A → ((¬¬(B → (¬A → A)) → ¬A) → (A → ¬(B → (¬A → A))))) → ((¬A → (¬¬(B → (¬A → A)) → ¬A)) → (¬A → (A → ¬(B → (¬A → A))))) LS2
13. (¬A → (¬¬(B → (¬A → A)) → ¬A)) → (¬A → (A → ¬(B → (¬A → A)))) MP 12,11
14. ¬A → (A → ¬(B → (¬A → A))) MP 13,8
15. (¬A → (A → ¬(B → (¬A → A)))) → ((¬A → A) → (¬A → ¬(B → (¬A → A)))) LS2
16. (¬A → A) → (¬A → ¬(B → (¬A → A))) MP 15,14
17. (¬A → ¬(B → (¬A → A))) → ((B → (¬A → A)) → A) LS3
18. ((¬A → ¬(B → (¬A → A))) → ((B → (¬A → A)) → A)) → ((¬A → A) → ((¬A → ¬(B → (¬A → A))) → ((B → (¬A → A)) → A))) LS1
19. (¬A → A) → ((¬A → ¬(B → (¬A → A))) → ((B → (¬A → A)) → A)) MP 18,17
20. ((¬A → A) → ((¬A → ¬(B → (¬A → A))) → ((B → (¬A → A)) → A))) → (((¬A → A) → (¬A → ¬(B → (¬A → A)))) → ((¬A → A) → ((B → (¬A → A)) → A))) LS2
21. ((¬A → A) → (¬A → ¬(B → (¬A → A)))) → ((¬A → A) → ((B → (¬A → A)) → A)) MP 20,19
22. (¬A → A) → ((B → (¬A → A)) → A) MP 21,16
23. (¬A → A) → (B → (¬A → A)) LS1
24. ((¬A → A) → ((B → (¬A → A)) → A)) → (((¬A → A) → (B → (¬A → A))) → ((¬A → A) → A)) LS2
25. ((¬A → A) → (B → (¬A → A))) → ((¬A → A) → A) MP 24,22
26. (¬A → A) → A MP 25,23
27. ¬¬A → (¬A → ¬¬A) LS1
28. (¬A → ¬¬A) → (¬A → A) LS3
29. ((¬A → ¬¬A) → (¬A → A)) → (¬¬A → ((¬A → ¬¬A) → (¬A → A))) LS1
30. ¬¬A → ((¬A → ¬¬A) → (¬A → A)) MP 29,28
31. (¬¬A → ((¬A → ¬¬A) → (¬A → A))) → ((¬¬A → (¬A → ¬¬A)) → (¬¬A → (¬A → A))) LS2
32. (¬¬A → (¬A → ¬¬A)) → (¬¬A → (¬A → A)) MP 31,30
33. ¬¬A → (¬A → A) MP 32,27
34. ((¬A → A) → A) → (¬¬A → ((¬A → A) → A)) LS1
35. ¬¬A → ((¬A → A) → A) MP 34,26
36. (¬¬A → ((¬A → A) → A)) → ((¬¬A → (¬A → A)) → (¬¬A → A)) LS2
37. (¬¬A → (¬A → A)) → (¬¬A → A) MP 36,35
38. ¬¬A → A MP 37,33
39. (¬¬A → A) → ((A → B) → (¬¬A → A)) LS1
40. (A → B) → (¬¬A → A) MP 39,38
41. ((A → B) → ((¬¬A → A) → (¬¬A → B))) → (((A → B) → (¬¬A → A)) → ((A → B) → (¬¬A → B))) LS2
42. ((A → B) → (¬¬A → A)) → ((A → B) → (¬¬A → B)) MP 41,7
43. (A → B) → (¬¬A → B) MP 42,40
44. ¬¬B → (¬¬(B → (¬¬B → ¬B)) → ¬¬B) LS1
45. (¬¬(B → (¬¬B → ¬B)) → ¬¬B) → (¬B → ¬(B → (¬¬B → ¬B))) LS3
46. ((¬¬(B → (¬¬B → ¬B)) → ¬¬B) → (¬B → ¬(B → (¬¬B → ¬B)))) → (¬¬B → ((¬¬(B → (¬¬B → ¬B)) → ¬¬B) → (¬B → ¬(B → (¬¬B → ¬B))))) LS1
47. ¬¬B → ((¬¬(B → (¬¬B → ¬B)) → ¬¬B) → (¬B → ¬(B → (¬¬B → ¬B)))) MP 46,45
48. (¬¬B → ((¬¬(B → (¬¬B → ¬B)) → ¬¬B) → (¬B → ¬(B → (¬¬B → ¬B))))) → ((¬¬B → (¬¬(B → (¬¬B → ¬B)) → ¬¬B)) → (¬¬B → (¬B → ¬(B → (¬¬B → ¬B))))) LS2
49. (¬¬B → (¬¬(B → (¬¬B → ¬B)) → ¬¬B)) → (¬¬B → (¬B → ¬(B → (¬¬B → ¬B)))) MP 48,47
50. ¬¬B → (¬B → ¬(B → (¬¬B → ¬B))) MP 49,44
51. (¬¬B → (¬B → ¬(B → (¬¬B → ¬B)))) → ((¬¬B → ¬B) → (¬¬B → ¬(B → (¬¬B → ¬B)))) LS2
52. (¬¬B → ¬B) → (¬¬B → ¬(B → (¬¬B → ¬B))) MP 51,50
53. (¬¬B → ¬(B → (¬¬B → ¬B))) → ((B → (¬¬B → ¬B)) → ¬B) LS3
54. ((¬¬B → ¬(B → (¬¬B → ¬B))) → ((B → (¬¬B → ¬B)) → ¬B)) → ((¬¬B → ¬B) → ((¬¬B → ¬(B → (¬¬B → ¬B))) → ((B → (¬¬B → ¬B)) → ¬B))) LS1
55. (¬¬B → ¬B) → ((¬¬B → ¬(B → (¬¬B → ¬B))) → ((B → (¬¬B → ¬B)) → ¬B)) MP 54,53
56. ((¬¬B → ¬B) → ((¬¬B → ¬(B → (¬¬B → ¬B))) → ((B → (¬¬B → ¬B)) → ¬B))) → (((¬¬B → ¬B) → (¬¬B → ¬(B → (¬¬B → ¬B)))) → ((¬¬B → ¬B) → ((B → (¬¬B → ¬B)) → ¬B))) LS2
57. ((¬¬B → ¬B) → (¬¬B → ¬(B → (¬¬B → ¬B)))) → ((¬¬B → ¬B) → ((B → (¬¬B → ¬B)) → ¬B)) MP 56,55
58. (¬¬B → ¬B) → ((B → (¬¬B → ¬B)) → ¬B) MP 57,52
59. (¬¬B → ¬B) → (B → (¬¬B → ¬B)) LS1
60. ((¬¬B → ¬B) → ((B → (¬¬B → ¬B)) → ¬B)) → (((¬¬B → ¬B) → (B → (¬¬B → ¬B))) → ((¬¬B → ¬B) → ¬B)) LS2
61. ((¬¬B → ¬B) → (B → (¬¬B → ¬B))) → ((¬¬B → ¬B) → ¬B) MP 60,58
62. (¬¬B → ¬B) → ¬B MP 61,59
63. ¬¬¬B → (¬¬B → ¬¬¬B) LS1
64. (¬¬B → ¬¬¬B) → (¬¬B → ¬B) LS3
65. ((¬¬B → ¬¬¬B) → (¬¬B → ¬B)) → (¬¬¬B → ((¬¬B → ¬¬¬B) → (¬¬B → ¬B))) LS1
66. ¬¬¬B → ((¬¬B → ¬¬¬B) → (¬¬B → ¬B)) MP 65,64
67. (¬¬¬B → ((¬¬B → ¬¬¬B) → (¬¬B → ¬B))) → ((¬¬¬B → (¬¬B → ¬¬¬B)) → (¬¬¬B → (¬¬B → ¬B))) LS2
68. (¬¬¬B → (¬¬B → ¬¬¬B)) → (¬¬¬B → (¬¬B → ¬B)) MP 67,66
69. ¬¬¬B → (¬¬B → ¬B) MP 68,63
70. ((¬¬B → ¬B) → ¬B) → (¬¬¬B → ((¬¬B → ¬B) → ¬B)) LS1
71. ¬¬¬B → ((¬¬B → ¬B) → ¬B) MP 70,62
72. (¬¬¬B → ((¬¬B → ¬B) → ¬B)) → ((¬¬¬B → (¬¬B → ¬B)) → (¬¬¬B → ¬B)) LS2
73. (¬¬¬B → (¬¬B → ¬B)) → (¬¬¬B → ¬B) MP 72,71
74. ¬¬¬B → ¬B MP 73,69
75. (¬¬¬B → ¬B) → (B → ¬¬B) LS3
76. B → ¬¬B MP 75,74
77. (B → ¬¬B) → (¬¬A → (B → ¬¬B)) LS1
78. ¬¬A → (B → ¬¬B) MP 77,76
79. (¬¬A → (B → ¬¬B)) → ((¬¬A → B) → (¬¬A → ¬¬B)) LS2
80. (¬¬A → B) → (¬¬A → ¬¬B) MP 79,78
81. ((¬¬A → B) → (¬¬A → ¬¬B)) → ((A → B) → ((¬¬A → B) → (¬¬A → ¬¬B))) LS1
82. (A → B) → ((¬¬A → B) → (¬¬A → ¬¬B)) MP 81,80
83. ((A → B) → ((¬¬A → B) → (¬¬A → ¬¬B))) → (((A → B) → (¬¬A → B)) → ((A → B) → (¬¬A → ¬¬B))) LS2
84. ((A → B) → (¬¬A → B)) → ((A → B) → (¬¬A → ¬¬B)) MP 83,82
85. (A → B) → (¬¬A → ¬¬B) MP 84,43
86. (¬¬A → ¬¬B) → (¬B → ¬A) LS3
87. ((¬¬A → ¬¬B) → (¬B → ¬A)) → ((A → B) → ((¬¬A → ¬¬B) → (¬B → ¬A))) LS1
88. (A → B) → ((¬¬A → ¬¬B) → (¬B → ¬A)) MP 87,86
89. ((A → B) → ((¬¬A → ¬¬B) → (¬B → ¬A))) → (((A → B) → (¬¬A → ¬¬B)) → ((A → B) → (¬B → ¬A))) LS2
90. ((A → B) → (¬¬A → ¬¬B)) → ((A → B) → (¬B → ¬A)) MP 89,88
91. (A → B) → (¬B → ¬A) MP 90,85

Try it online!
A more human-readable version using 5 lemmas:
Lemma 1: From A → B and B → C, instantiate A → C. (5 steps)

1. B → C                                         given
2. (B → C) → (A → (B → C))                       L.S.1
3. A → (B → C)                                   M.P. (1,2)
4. (A → (B → C)) → ((A → B) → (A → C))           L.S.2
5. (A → B) → (A → C)                             M.P. (3,4)
6. A → B                                         given
7. A → C                                         M.P. (6,5)

Lemma 2: ¬A → (A → B) (7 steps)

1. ¬A → (¬B → ¬A)                                L.S.1
2. (¬B → ¬A) → (A → B)                           L.S.3
3. ¬A → (A → B)                                  Lemma 1 (1,2)

Lemma 3: From A → (B → C) and A → B, instantiate A → C. (3 steps)

1. A → (B → C)                                   given
2. (A → (B → C)) → ((A → B) → (A → C))           L.S.2
3. (A → B) → (A → C)                             M.P. (1,2)
4. A → B                                         given
5. A → C                                         M.P. (4,3)

Lemma 4: ¬¬A → A (31 steps)

1. ¬A → (A → ¬(B → (¬A → A)))                    Lemma 2
2. (¬A → (A → ¬(B → (¬A → A)))) →
   ((¬A → A) → (¬A → ¬(B → (¬A → A))))           L.S.2
3. (¬A → A) → (¬A → ¬(B → (¬A → A)))             M.P. (1,2)
4. (¬A → ¬(B → (¬A → A))) →((B → (¬A → A)) → A)  L.S.3
5. (¬A → A) → ((B → (¬A → A)) → A)               Lemma 1 (3,4)
6. (¬A → A) → (B → (¬A → A))                     L.S.1
7. (¬A → A) → A                                  Lemma 3 (5,6)
8. ¬¬A → (¬A → A)                                Lemma 2
9. ¬¬A → A                                       Lemma 1 (8,7)

Lemma 5: (A → B) → (¬¬A → B) (43 steps)

1. (A → B) → (¬¬A → (A → B))                     L.S.1
2. (¬¬A → (A → B)) → ((¬¬A → A) → (¬¬A → B))     L.S.2
3. (A → B) → ((¬¬A → A) → (¬¬A → B))             Lemma 1 (1,2)
4. ¬¬A → A                                       Lemma 4
5. (¬¬A → A) → ((A → B) → (¬¬A → A))             L.S.1
6. (A → B) → (¬¬A → A)                           M.P. (4,5)
7. (A → B) → (¬¬A → B)                           Lemma 3 (3,6)

Theorem: (A → B) → (¬B → ¬A)

1. (A → B) → (¬¬A → B)                           Lemma 5
2. ¬¬¬B → ¬B                                     Lemma 4
3. (¬¬¬B → ¬B) → (B → ¬¬B)                       L.S.3
4. B → ¬¬B                                       M.P. (2,3)
5. (B → ¬¬B) → (¬¬A → (B → ¬¬B))                 L.S.1
6. ¬¬A → (B → ¬¬B)                               M.P. (4,5)
7. (¬¬A → (B → ¬¬B)) → ((¬¬A → B) → (¬¬A → ¬¬B)) L.S.2
8. (¬¬A → B) → (¬¬A → ¬¬B)                       M.P. (6,7)
9. (A → B) → (¬¬A → ¬¬B)                         Lemma 1 (1,8)
10.(¬¬A → ¬¬B) → (¬B → ¬A)                       L.S.3
11.(A → B) → (¬B → ¬A)                           Lemma 1 (9,10)

Welcome to the site and impressive answer! Have you verified your answer with the Prolog script? If so, would you mind including a link to said verification?

@cairdcoinheringaahing I've added a tio link to the prolog script to the answer so that it can be verified (it does work).  Usually I would comment the link but the link is too long to fit in a comment.

That's basically the proof I was in the process of making, except that you used different lemmas. I used the Principle of Identity. Also, I hadn't proved Double Negation Elimination yet, because the proof of that I was creating required Contradiction Realization.

Would you be able to cut out Lemma 5 and instead prove and use the Substitution Theorem to get from (¬¬A → ¬¬B) → (¬B → ¬A) to (A → B) → (¬B → ¬A) in fewer steps?

I think the very first step is redundant?  I couldn't find anything referencing it so I tried running it on TIO without that line and didn't get any "Invalid step" warnings.

@Antony Step 7 uses step 1 and 6.

@user56656 oops, OK thanks.

@mbomb007 Proving the substitution theorem in this particular case seems to require repeating the steps here. I don't think it will be shorter.

59 steps
Norman Megill, author of Metamath has told me about a 59 step proof, which I'm going to post here in this community wiki.  The original can be found in theorem 2.16 on this page.
http://us.metamath.org/mmsolitaire/pmproofs.txt
Norm says: This page would provide plenty of challenges for you to beat!
Here's the proof
((P -> Q) -> (~ Q -> ~ P)); ! *2.16
((P -> Q) -> (~ Q -> ~ P)); ! Result of proof
DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311
; ! 59 steps

The proof is in Polish notation, so it starts from the conclusion and
continues backwards until every term has been satisified by an axiom.
The character mapping is as follows:  "1" is LS axiom 1, "2" is LS axiom 2, "3"
is LS axiom 3, and "D" is Modus Ponens.
Here's the proof in @W-W's suggested format
01 ax-1          $a |- ( ¬ ¬ ¬ B → ( ¬ B → ¬ ¬ ¬ B ) )
02 ax-1          $a |- ( ¬ ¬ ¬ B → ( ¬ ¬ ( ¬ B → ¬ ¬ ¬ B ) → ¬ ¬ ¬ B ) )
03 ax-3          $a |- ( ( ¬ ¬ ( ¬ B → ¬ ¬ ¬ B ) → ¬ ¬ ¬ B ) → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) )
04 ax-1          $a |- ( ( ( ¬ ¬ ( ¬ B → ¬ ¬ ¬ B ) → ¬ ¬ ¬ B ) → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) ) → ( ¬ ¬ ¬ B → ( ( ¬ ¬ ( ¬ B → ¬ ¬ ¬ B ) → ¬ ¬ ¬ B ) → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) ) ) )
05 3,4 ax-mp     $a |- ( ¬ ¬ ¬ B → ( ( ¬ ¬ ( ¬ B → ¬ ¬ ¬ B ) → ¬ ¬ ¬ B ) → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) ) )
06 ax-2          $a |- ( ( ¬ ¬ ¬ B → ( ( ¬ ¬ ( ¬ B → ¬ ¬ ¬ B ) → ¬ ¬ ¬ B ) → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) ) ) → ( ( ¬ ¬ ¬ B → ( ¬ ¬ ( ¬ B → ¬ ¬ ¬ B ) → ¬ ¬ ¬ B ) ) → ( ¬ ¬ ¬ B → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) ) ) )
07 5,6 ax-mp     $a |- ( ( ¬ ¬ ¬ B → ( ¬ ¬ ( ¬ B → ¬ ¬ ¬ B ) → ¬ ¬ ¬ B ) ) → ( ¬ ¬ ¬ B → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) ) )
08 2,7 ax-mp     $a |- ( ¬ ¬ ¬ B → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) )
09 ax-3          $a |- ( ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) )
10 ax-1          $a |- ( ( ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) ) → ( ¬ ¬ ¬ B → ( ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) ) ) )
11 9,10 ax-mp    $a |- ( ¬ ¬ ¬ B → ( ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) ) )
12 ax-2          $a |- ( ( ¬ ¬ ¬ B → ( ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) ) ) → ( ( ¬ ¬ ¬ B → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) ) → ( ¬ ¬ ¬ B → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) ) ) )
13 11,12 ax-mp   $a |- ( ( ¬ ¬ ¬ B → ( ¬ ¬ B → ¬ ( ¬ B → ¬ ¬ ¬ B ) ) ) → ( ¬ ¬ ¬ B → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) ) )
14 8,13 ax-mp    $a |- ( ¬ ¬ ¬ B → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) )
15 ax-2          $a |- ( ( ¬ ¬ ¬ B → ( ( ¬ B → ¬ ¬ ¬ B ) → ¬ B ) ) → ( ( ¬ ¬ ¬ B → ( ¬ B → ¬ ¬ ¬ B ) ) → ( ¬ ¬ ¬ B → ¬ B ) ) )
16 14,15 ax-mp   $a |- ( ( ¬ ¬ ¬ B → ( ¬ B → ¬ ¬ ¬ B ) ) → ( ¬ ¬ ¬ B → ¬ B ) )
17 1,16 ax-mp    $a |- ( ¬ ¬ ¬ B → ¬ B )
18 ax-3          $a |- ( ( ¬ ¬ ¬ B → ¬ B ) → ( B → ¬ ¬ B ) )
19 17,18 ax-mp   $a |- ( B → ¬ ¬ B )
20 ax-1          $a |- ( ( B → ¬ ¬ B ) → ( A → ( B → ¬ ¬ B ) ) )
21 19,20 ax-mp   $a |- ( A → ( B → ¬ ¬ B ) )
22 ax-2          $a |- ( ( A → ( B → ¬ ¬ B ) ) → ( ( A → B ) → ( A → ¬ ¬ B ) ) )
23 21,22 ax-mp   $a |- ( ( A → B ) → ( A → ¬ ¬ B ) )
24 ax-1          $a |- ( ( A → ¬ ¬ B ) → ( ¬ ¬ A → ( A → ¬ ¬ B ) ) )
25 ax-1          $a |- ( ¬ ¬ A → ( ¬ ¬ ( A → ¬ ¬ B ) → ¬ ¬ A ) )
26 ax-3          $a |- ( ( ¬ ¬ ( A → ¬ ¬ B ) → ¬ ¬ A ) → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) )
27 ax-1          $a |- ( ( ( ¬ ¬ ( A → ¬ ¬ B ) → ¬ ¬ A ) → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) ) → ( ¬ ¬ A → ( ( ¬ ¬ ( A → ¬ ¬ B ) → ¬ ¬ A ) → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) ) ) )
28 26,27 ax-mp   $a |- ( ¬ ¬ A → ( ( ¬ ¬ ( A → ¬ ¬ B ) → ¬ ¬ A ) → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) ) )
29 ax-2          $a |- ( ( ¬ ¬ A → ( ( ¬ ¬ ( A → ¬ ¬ B ) → ¬ ¬ A ) → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) ) ) → ( ( ¬ ¬ A → ( ¬ ¬ ( A → ¬ ¬ B ) → ¬ ¬ A ) ) → ( ¬ ¬ A → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) ) ) )
30 28,29 ax-mp   $a |- ( ( ¬ ¬ A → ( ¬ ¬ ( A → ¬ ¬ B ) → ¬ ¬ A ) ) → ( ¬ ¬ A → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) ) )
31 25,30 ax-mp   $a |- ( ¬ ¬ A → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) )
32 ax-3          $a |- ( ( ¬ A → ¬ ( A → ¬ ¬ B ) ) → ( ( A → ¬ ¬ B ) → A ) )
33 ax-1          $a |- ( ( ( ¬ A → ¬ ( A → ¬ ¬ B ) ) → ( ( A → ¬ ¬ B ) → A ) ) → ( ¬ ¬ A → ( ( ¬ A → ¬ ( A → ¬ ¬ B ) ) → ( ( A → ¬ ¬ B ) → A ) ) ) )
34 32,33 ax-mp   $a |- ( ¬ ¬ A → ( ( ¬ A → ¬ ( A → ¬ ¬ B ) ) → ( ( A → ¬ ¬ B ) → A ) ) )
35 ax-2          $a |- ( ( ¬ ¬ A → ( ( ¬ A → ¬ ( A → ¬ ¬ B ) ) → ( ( A → ¬ ¬ B ) → A ) ) ) → ( ( ¬ ¬ A → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) ) → ( ¬ ¬ A → ( ( A → ¬ ¬ B ) → A ) ) ) )
36 34,35 ax-mp   $a |- ( ( ¬ ¬ A → ( ¬ A → ¬ ( A → ¬ ¬ B ) ) ) → ( ¬ ¬ A → ( ( A → ¬ ¬ B ) → A ) ) )
37 31,36 ax-mp   $a |- ( ¬ ¬ A → ( ( A → ¬ ¬ B ) → A ) )
38 ax-2          $a |- ( ( ¬ ¬ A → ( ( A → ¬ ¬ B ) → A ) ) → ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → A ) ) )
39 37,38 ax-mp   $a |- ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → A ) )
40 ax-2          $a |- ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ( ¬ ¬ A → A ) → ( ¬ ¬ A → ¬ ¬ B ) ) )
41 ax-2          $a |- ( ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ( ¬ ¬ A → A ) → ( ¬ ¬ A → ¬ ¬ B ) ) ) → ( ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → A ) ) → ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → ¬ ¬ B ) ) ) )
42 40,41 ax-mp   $a |- ( ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → A ) ) → ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → ¬ ¬ B ) ) )
43 39,42 ax-mp   $a |- ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → ¬ ¬ B ) )
44 ax-1          $a |- ( ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → ¬ ¬ B ) ) → ( ( A → ¬ ¬ B ) → ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → ¬ ¬ B ) ) ) )
45 43,44 ax-mp   $a |- ( ( A → ¬ ¬ B ) → ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → ¬ ¬ B ) ) )
46 ax-2          $a |- ( ( ( A → ¬ ¬ B ) → ( ( ¬ ¬ A → ( A → ¬ ¬ B ) ) → ( ¬ ¬ A → ¬ ¬ B ) ) ) → ( ( ( A → ¬ ¬ B ) → ( ¬ ¬ A → ( A → ¬ ¬ B ) ) ) → ( ( A → ¬ ¬ B ) → ( ¬ ¬ A → ¬ ¬ B ) ) ) )
47 45,46 ax-mp   $a |- ( ( ( A → ¬ ¬ B ) → ( ¬ ¬ A → ( A → ¬ ¬ B ) ) ) → ( ( A → ¬ ¬ B ) → ( ¬ ¬ A → ¬ ¬ B ) ) )
48 24,47 ax-mp   $a |- ( ( A → ¬ ¬ B ) → ( ¬ ¬ A → ¬ ¬ B ) )
49 ax-3          $a |- ( ( ¬ ¬ A → ¬ ¬ B ) → ( ¬ B → ¬ A ) )
50 ax-1          $a |- ( ( ( ¬ ¬ A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) → ( ( A → ¬ ¬ B ) → ( ( ¬ ¬ A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) ) )
51 49,50 ax-mp   $a |- ( ( A → ¬ ¬ B ) → ( ( ¬ ¬ A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) )
52 ax-2          $a |- ( ( ( A → ¬ ¬ B ) → ( ( ¬ ¬ A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) ) → ( ( ( A → ¬ ¬ B ) → ( ¬ ¬ A → ¬ ¬ B ) ) → ( ( A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) ) )
53 51,52 ax-mp   $a |- ( ( ( A → ¬ ¬ B ) → ( ¬ ¬ A → ¬ ¬ B ) ) → ( ( A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) )
54 48,53 ax-mp   $a |- ( ( A → ¬ ¬ B ) → ( ¬ B → ¬ A ) )
55 ax-1          $a |- ( ( ( A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) → ( ( A → B ) → ( ( A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) ) )
56 54,55 ax-mp   $a |- ( ( A → B ) → ( ( A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) )
57 ax-2          $a |- ( ( ( A → B ) → ( ( A → ¬ ¬ B ) → ( ¬ B → ¬ A ) ) ) → ( ( ( A → B ) → ( A → ¬ ¬ B ) ) → ( ( A → B ) → ( ¬ B → ¬ A ) ) ) )
58 56,57 ax-mp   $a |- ( ( ( A → B ) → ( A → ¬ ¬ B ) ) → ( ( A → B ) → ( ¬ B → ¬ A ) ) )
59 23,58 ax-mp   $a |- ( ( A → B ) → ( ¬ B → ¬ A ) )

Try it online!
Here it is in The Incredible Proof Machine

png svg

I don't remember suggesting such a format... For what it's worth, the corresponding sk expression is s(k(s(k c)(s(k(s s(s(s(k c)(s(k c)k)))))k)))(s(k(c(s(s(k c)(s(k c)k))k)))). I don't have a way to convert that back to lambdas though

@H.PWiz It’s \x -> c (\y -> c (\z -> c (c (\_ -> z)) (\_ -> z)) (x (c (c (\_ -> y)) (\z -> c (\t -> c (c (\_ -> t)) (\_ -> t)) (x z))))). (Probably not what you’d write if you were approaching it from that direction.)

@AndersKaseorg Yeah, I just found that and extracted out the useful theorems: here

@H.PWiz, sorry, no you didn't suggest that format.  I meant that (stripped of the margin) it is compatible with your Prolog verifier.

@H.PWiz also - oh dear - I slightly garbled that version of the proof when I put the margin in.  Fixed now.

@Antony The prolog verifier is written by WW, the author of the question

I'm sorry for mistaking you for OP, @H.PWiz  I'm afraid your username looked like one in the succession of WW's many names https://i.imgur.com/VoSVoqI.png

Using pmGenerator, the following command prints the full proof with formulas in infix notation: pmGenerator --parse DD2D1DD2D13DD2D1DD22D2DD2D13DD2D1311D2D1D3DD2DD2D13DD2D1311 -u. Append -j -1 to that command in order to not split up subproofs that are used multiple times, or -j 1 to split up into all subproofs. These commands also validate the proof.

all_licenses: Creative Commons - Attribution Share-Alike - https://creativecommons.org/licenses/by-sa/4.0/