text:
How on earth did llhuii output the Evil Numbers in 42 bytes of Python?
This is a tips question for golfing in Python concerning the Evil Numbers question on Anarchy Golf.
An number is evil if its binary expansion has an even number of 1's. The challenge is to print the first 400 evil numbers 0,3,5,...,795,797,798, one per line.
The Python 2 submissions are led by llhuii with a 42-byte solution. The next best is 46 bytes by mitchs, followed by five 47-byte submissions. It seems llhuii has found something truly magical that has eluded many strong Python golfers for over 2 years. Saving 4 or 5 bytes is huge for such a short golf.

I'm still at 47 bytes. I'm hoping we can crack this puzzle as a community. If we get an answer jointly, I'd submit it under the names of everyone who contributed. An answer to this question can be a piece of code or a new idea or a piece of analysis. If you are llhuii, please don't spoil it for us yet.
Though submissions are not revealed because this problem is Endless, we're given some leads. The winning submission took 0.1699 seconds to run, much longer than any other, suggesting an inefficient method. From the byte statistics, of the 42 characters, 23 are alphanumeric [0-9A-Za-z] and 19 are ASCII symbols. This means there is no whitespace in llhuii's solution.
You can test your code on the problem page, choosing Python from the language dropdown or uploading a .py file. Note that:

Python 2.7 is used
Your code must be a full program that prints
There's no input for this problem, like kolmogorov-complexity
Your program just has to print the 400 values as given, even if it would break on larger values
Programs have 2 seconds to run
Programs may terminate with error
You may use exec; the "exec is denied" refers to shell exec

It may also be worthy to note that this sequences is "Indices of zeros in the Thue-Morse sequence A010060." (source: oeis)

Now it's 40/41 bytes :P

This isn't the same solution as llhuii's, but it's also 42 bytes long.
n=0;exec'print n;n^=(n^n+2)%3/2;n+=2;'*400

Try it online!
Thanks to @JonathanFrech, we're now at 40 bytes.
n=0;exec'print n;n=n+2^(n^n+2)/2%3;'*400

Try it online!
There's another byte to be saved, for a total of 39.
n=0;exec'print n;n=n+2^-(n^n+2)%3;'*400

Try it online!

Out of curiosity, how do you know the 42-byte version is not the same as  llhuii's? (I have never participated in Anarchy Golf)

@LuisMendo The Statistics tab lists 23 alphanumerical bytes and 19 ASCII symbols, so there's no whitespace. Unless llhuii wrote print+n, their solution must be different from mine.

Ah, so you can get some information even if you don't know the code. That's nice. Thanks!

Do you think there's chance for a 38? In theory there are some degrees of freedom to potentially remove the - sign by shifting with print~n or print-n and using & or ~, though I haven't gotten anything to work. Also, n=0;exec"print n;d=n^n+2;n^=d^-d%3;"*400 is pretty but 40 bytes.

print-n seems unlikely as there is no easy relationship between the set bits of n and -n. print~n sounds more promising in theory, but I can't get below 40 bytes with this approach.

Getting 39 bytes
This is an explanation of how I got a 39-byte solution, which Dennis and JonathanFrech found separately as well. Or, rather, it explains how one could arrive at the answer in hindsight, in a way that's much nicer than my actual path to it, which was full of muddy reasoning and dead ends.
n=0
exec"print n;n=n+2^-(n+2^n)%3;"*400

Writing this a bit less golfed and with more parens, this looks like:
n=0
for _ in range(400):
  print n
  n=(n+2)^(-((n+2)^n))%3

Bit parities
We start with an idea from my 47-byte solution to output all numbers of the form n=2*k+b where k counts up 0,1,...,399 and b is a parity bit that makes the overall number of 1's even.
Let's write par(x) for the bit parity of x, that is the xor (^) all of bits in x. This is 0 if there's an even number of 1-bits (number is evil), and 1 if there's an odd number of 1-bits. For n=2*k+b, we have par(n) = par(k)^b, so to achieve evil par(n)==0 we need b=par(k), i.e. the last bit of n to be the bit parity of the preceding bits.
My first efforts at golfing were on expressing the par(k), at first directly with bin(k).count('1')%2, and then with bit manipulation.
Parity updates
Still, there didn't seem to be a short expression. Instead, it helped to realize that there's more info to work with. Rather than just computing the bit parity of the current number,
k  ---->  par(k)

we can update the bit parity as we increment k to k+1.
k   ---->  par(k)
      |
      v
k+1 ---->  par(k+1)

That is, since we're counting up k=0,1,2,..., we merely need to maintain the current bit parity rather than calculating it from scratch each time. The bit parity update par(k+1)^par(k) is the parity of the number of bits flipped in going from k to k+1, that is par((k+1)^k).
par(k+1) ^ par(k) = par((k+1)^k)
par(k+1) = par(k) ^ par((k+1)^k)

Form of (k+1)^k
Now we need to compute par((k+1)^k). It might seem like we've gotten nowhere because computing bit parity is exactly the problem we're trying to solve. But, numbers expressed as (k+1)^k have the form 1,3,7,15,.., that is one below a power of 2, a fact often used in bit hacks. Let's see why that is.
When we increment k, the effect of the binary carries is to invert the last 0 and all 1's to its right, creating a new leading 0 if there were none. For example, take k=43=0b101011
      **
  101011  (43)
 +     1
  ------
= 101100  (44)

  101011  (43)
 ^101100  (44)
  ------
= 000111  (77)

The columns causing a carry are marked with *. These have a 1 change to a 0 and pass on a carry bit of 1, which keeps propagating left until it hits a 0 in k, which changes to 1. Any bits further to the left are unaffected. So, when k^(k+1) checks which bit positions change k to k+1, it finds the positions of the rightmost 0 and the 1's to its right. That is, the changed bits form a suffix, so result is 0's followed by one or more 1's. Without the leading zeroes, there are binary numbers 1, 11, 111, 1111, ... that are one below a power of 2.
Computing par((k+1)^k)
Now that we understand that (k+1)^k is limited to 1,3,7,15,..., let's find a way to compute the bit parity of such numbers. Here, a useful fact is that 1,2,4,8,16,... alternate modulo 3 between 1 and 2, since 2==-1 mod 3 . So, taking 1,3,7,15,31,63... modulo 3 gives 1,0,1,0,1,0..., which are exactly their bit parities. Perfect!
So, we can do the update par(k+1) = par(k) ^ par((k+1)^k) as
par(k+1) = par(k) ^ ((k+1)^k)%3

Using b as the variable we're storing the parity in, this looks like
b^=((k+1)^k)%3

Writing the code
Putting this together in code, we start k and the parity bit b both at 0, then repeatedly print n=2*k+b and update b=b^((k+1)^k)%3 and k=k+1.
46 bytes
k=b=0
exec"print 2*k+b;b^=(k+1^k)%3;k+=1;"*400

Try it online!
We removed parens around k+1 in ((k+1)^k)%3 because Python precedence does the addition first anyway, weird as it looks.
Code improvements
We can do better though by working directly with a single variable n=2*k+b and performing the updates directly on it. Doing k+=1 corresponds to n+=2. And, updating b^=(k+1^k)%3 corresponds to n^=(k+1^k)%3. Here, k=n/2 before updating n.
44 bytes
n=0
exec"print n;n^=(n/2+1^n/2)%3;n+=2;"*400

Try it online!
We can shorten n/2+1^n/2 (remember this is (n/2+1)^n/2) by rewriting
n/2+1 ^ n/2
(n+2)/2 ^ n/2
(n+2 ^ n)/2

Since /2 removes the last bit, it doesn't matter if we do it before or after xor-ing. So, we have n^=(n+2^n)/2%3. We can save another byte by noting that modulo 3, /2 is equivalent to *2 is equivalent to -, noting that n+2^n is even so the division is actual halving without flooring. This gives n^=-(n+2^n)%3
41 bytes
n=0
exec"print n;n^=-(n+2^n)%3;n+=2;"*400

Try it online!
Finally, we can combine the operations n^=c;n+=2 into n=(n+2)^c, where c is a bit. This works because ^c acts only on the last bit and +2 doesn't care about the last bit, so the operations commute. Again, precedence lets us omit parens and write n=n+2^c.
39 bytes
n=0
exec"print n;n=n+2^-(n+2^n)%3;"*400

Try it online!

This gives my (xnor's) 47-byte solution and the thinking that led me to it. Don't read this if you want to figure this out yourself.
A natural first idea is to iterate through the numbers 0 to 799, printing only those with an even number of 1's in binary.
52 bytes
for n in range(800):
 if~bin(n).count('1')%2:print n

Try it online!
Here, the ~ takes the bit complement so as to switch even<->odd in the count and give a truthy value only on even counts.
We can improve this method by generating all the values instead of filtering. Observe that the output values are the numbers 0 to 399, each with a bit appended to make the number of 1 bits even.
0 = 2*0 + 0
3 = 2*1 + 1
5 = 2*2 + 1
6 = 2*3 + 0
...

So, the nth number is either 2*n+b with either b=0 or b=1. The bit b can be found by counting 1's in the bits of n and taking the count modulo 2.
49 bytes
for n in range(400):print 2*n+bin(n).count('1')%2

Try it online!
We can cut the 2 bytes for 2* by iterating over 0,2,4,..., which doesn't chance the count of 1's. We can do this by using an exec loop that runs 400 times and increasing n by 2 each loop.
47 bytes
n=0;exec"print n+bin(n).count('1')%2;n+=2;"*400

Try it online!
And, that's my 47-byte solution. I suspect most if not all the other 47-byte solutions are the same.

Is your 47 bytes long exec-approach allowed?

@JonathanFrech Yes, when the page says "exec is denied", it's not referring to Python's exec but the command line exec.

llhuii’s Python 3 submission
Here are the Python 3 submissions for Evil Numbers at the time of writing:

llhuii probably ported their trick to Python 3, and came up with a solution that is

3 bytes longer than their Python 2 solution, and
has 45 − (25 + 18) = 2 bytes of whitespace.

Porting xnor’s 47B to Python 3 literally, we get this 50B:
n=0;exec("print(n+bin(n).count('1')%2);n+=2;"*400)

I submitted it as ppcg(xnor). (It adds parentheses to exec and print, which are now functions.) It has different code stats from the other Python 3 answers, which all have some amount of whitespace in them. Interesting!
There’s a shorter way to rewrite it though (exec tends to lose its competitive edge in Python 3):
n=0
while n<800:print(n+bin(n).count('1')%2);n+=2

It’s 49 bytes. I submitted it as ppcg(xnor,alternative). This has two bytes of whitespace, just like llhui’s answer! This leads me to believe that llhuii’s Python 3 answer looks kinda like this (newline, then a while loop.) So llhuii probably used exec in Python 2 and while in Python 3, just like us; this explains the whitespace discrepancy.

Our 47B became a 49B in Python 3. What’s interesting, now, is that llhuii’s 42B didn’t become a 44B, it became a 45B! Something about llhuii’s solution takes one byte extra in Python 3. This could mean a variety of things.

The first thing that comes to mind is division: maybe llhuii uses / in Python 2, which became // in Python 3. (If they’re counting in twos like us, then n/2 might be used to shift n back to the right by one bit?)
The other thing that comes to mind is unary operators after print. Our print blah became print(blah) (1 byte extra), but if llhuii wrote something like print~-blah in Python 2, it’d become print(~-blah) in Python 3.
Maybe there are other ideas. Please let me know.

Code statistics for all Py3 solutions, including mine now:

What I find interesting is that their Python 3 solution is significantly faster than their Python 2 solution. Either they are using some Python feature that got more efficient in Python 3 or it is not a simple port after all (maybe they found a Python 3 solution which is shorter than a direct port would be).

The runtimes on anagol have huge variance, I commented on the OP that llhuii’s runtime here makes me think that their Py2 runtime is just a red herring/outlier

Also, I assume xnor found a very similar trick and improved on it (there can’t be that many ways to print evil numbers, right?!) and their solution is plenty fast!

Other approaches
1) Using a formula for A001969
Rather than converting to binary, it might be possible to take advantage of the following formula (from OEIS):

a(1) = 0
for n > 1: a(n) = 3*n-3-a(n/2) if n is even
           a(n) = a((n+1)/2)+n-1 if n is odd

I'm very bad at golfing in Python, so I'm not even going to try. But here is a quick attempt in JS.
NB: I don't think it would be a valid JS submission as it's just filling an array without displaying it. And even so, it's 5 bytes longer than the current best JS solution (which is 45 bytes). But that's not the point here anyway.
for(a=[n=0,3];n<199;)a.push(2*++n+a[n],6*n+3-a[n])

for(a=[n=0,3];n<199;)a.push(2*++n+a[n],6*n+3-a[n])

console.log(a.join`, `)

Hopefully it may give some inspiration.
Using an array is probably not a good idea because it needs to be initialized and updated. It might be more efficient (code size wise) to use a recursive function instead, which would explain why the winning solution is taking more time than the other ones.
2) Building the Thue-Morse sequence with substitutions
In theory, this code should work:
n=0;a="1";b="0";exec"t=a;a+=b;b+=t;print(int(b[n]))+n;n+=2;"*400

Try it online! (runnable version limited to 20 terms)
It computes the Thue-Morse sequence with consecutive substitutions and looks for the position of 1's (Evil Numbers) in the same loop.
But:

It's far too long in its current form
It quickly leads to a memory overflow

3) Building the Thue-Morse sequence with bitwise operations
Starting from Wikipedia's Direct Definition of the Thue-Morse sequence, I've come to this algorithm (switching back to JS ... sorry):
for(e=n=0;n<799;)(e^=!(((x=n++^n)^x/2)&170))||console.log(n)

where we keep track of the current evilness of the sequence in e and use 170 as a bitmask of odd bits in a byte.

I like the idea of a recursive function, but Python is very bad at that for boilerplate: f=lambda n:_ for n in range(400):print f(n) already takes 43 bytes. Maybe there's a way to simulate the recursion by building an array that references itself, or an array that adds future elements to the end.

Also, llhuii's solution has no spaces in it, so he didn't use def, for, while, lambda (with a parameter at least), etc.

@Stephen Something like while~0:print~1 does not require any spaces.

In method number 3, ((x=n++^n)^x/2) seems somewhat verbose just to find the lowest set bit. That whole mess can be replaced by ++n&-n. Try it online!

@primo I've no idea what I was thinking here and how I came to this cumbersome formula. ¯\(ツ)/¯

In your defense, it's a direct translation of what's written on the wikipedia page. FWIW, I recently shaved 3 strokes off my bash solution using this method.

By construction, n+n^n is always evil, but my poor Python skills could only come up with a 61-byte solution:
for n in sorted(map(lambda n:n+n^n,range(512)))[:400]:print n

Thanks to @Peilonrayz for saving 5 bytes and @Mr.Xcoder for saving 1 byte:
for n in sorted(n^n*2for n in range(512))[:400]:print n

55 bytes: for n in sorted(n^n*2for n in range(512))[:400]:print n. n+n^n is the same as n^n*2

Idea: Shorter bit parity
It takes many characters to do bin(n).count('1')%2 to compute the parity of the bit-count. Maybe an arithmetic way is shorter, especially given a limited bit length.
A cute same-length way is int(bin(n)[2:],3)%2, interpreting the binary value as base 3 (or any odd base). Unfortunately, 4 of the bytes are spend removing the 0b prefix. It also works to do int(bin(n)[2:])%9%2.
Another idea comes from combining bits using xor. If n has binary representation abcdefghi, then
n/16 = abcde
n%16 =  fghi

r = n/16 ^ n%16 has binary representation (a)(b^f)(c^g)(d^h)(e^i)

So, r=n/16^n%16 is evil if and only if n is evil. We can then repeat that as s=r/4^r%4, a value s in 0,1,2,3, of which 1 and 2 are not evil, checkable with 0<s<3.
52 bytes
n=0;exec"r=n/16^n%16;print(0<r/4^r%4<3)+n;n+=2;"*400

Try it online!
This turned out a good deal longer. There's many knobs to turn though of how to split the number, how to check the final number (maybe a bit-based lookup table). I suspect these can only go so far though.

would it be a possibility to use the to_bytes function of integers? I doubt it but something to consider :)

@HyperNeutrino I think that's Python 3 only?

yup my bad :/ rip

exec'^'.join(bin(n)[2:]) is another fun way, but way too long I think.

Simply use the 0b: int(bin(n),13)%2! :D

Progress! Noodle9’s trick offers a 44-byte solution: n=0;exec"print~int(bin(n),13)%2+n;n+=2;"*400

Nested counters approach
I have an idea for a different approach, but I am not experienced enough in python golfing, so I'll leave it here for you guys to consider as another possible starting point for golfing.
The ungolfed idea:
n=0
i=1
for _ in"01":
 i^=1
 for _ in"01":
  i^=1
  for _ in"01":
   i^=1
   for _ in"01":
    i^=1
    for _ in"01":
     i^=1
     for _ in"01":
      i^=1
      for _ in"01":
       i^=1
       for _ in"01":
        i^=1
        for _ in"01":
          i^=1
          if n<800:print i+n
          n+=2

Try it online!
Nine levels nesting depth, all the loops are the same, so in my mind they should be built by exec"something"*9+"deepest stuff". In practice I don't know if it is possible to do something like this with a for cycle.
Things to consider for golfing:

maybe there is some other possibility to cycle twice other than a for loop (I tried a quine-like approach with the string to be executed passed to itself as a formatting argument twice,but my head exploded).
there could also be a better alternative to if n<800:, which is needed here because otherwise we would keep printing evil numbers up to 2^10

116 bytes.

Maybe try nested list comprehensions instead of nested for loops?

@Sparr The problem then is to actually print the numbers. In Python 2, print is a statement, not a function, and thus cannot appear inside a comprehension.

maybe print '\n'.join([[[[[[[[[foo]foo]foo]foo]foo]foo]foo]foo]foo])

@Sparr Then the problem lies in flattening the list; str.join only works on lists containing strings and the extra list characters must not be printed. Formatting alone would take a significant amount of bytes.

Idea: Reduce over XOR
If you XOR all the bits of n together, it will be 0 for evil and 1 for non-evil. You can do this with a recursive function (which may have thus taken more time?), like so:
f=lambda n:f(n/2^n&1)if n>1else-~-n

This returns 1 for evil.
That's 35 bytes, and checks whether or not a number is evil. Unfortunately, filter is already 6 bytes so this wasn't the optimal solution verbatim but this idea can probably be golfed.

I think you can do f=lambda n:n>1and f(n/2^n&1)or-~-n for -1 byte.

@EriktheOutgolfer I tried but that causes errors when f(n/2^n&1) returns 0...

Substitution method : {1 -> {1, -1}, -1 -> {-1, 1}}
You can also make this substitution 10 times {1 -> {1, -1}, -1 -> {-1, 1}}, then flatten and check the positions of 1's
here is the mathematica code
(F = Flatten)@
Position[F@Nest[#/.{1->{1,-1},-1->{-1,1}}&,1,10],1][[;; 400]] - 1

How would you do this in python?

Idea: A006068 (“a(n) is Gray-coded into n”)
Neil’s idea of sorting all the 2n XOR n intrigued me, so I tried to find the indices behind this sort. I wrote this code, and it reveals that we can write something like this:
for n in range(400):x=a(n);print 2*x^x

Where a(n) is A006068(n). Try it online!
However, this assumes we have some short way to compute A006068. This is already 38 bytes, assuming we can calculate it in 4 bytes (the a(n) part). The real implementation (in the TIO header) is far longer than that. Not much hope for this I think.


text:
Increasing, decreasing, none or all?
Take two inputs, a non-empty vector/list containing digits 1 and 2 and a string (no, you may not take 0/1 instead). The string will be one of the following (in lowercase, exactly as written below:
increasing
decreasing
ones
twos
all
none

If the string is ____ then you shall return the indices ___:

increasing ... where the list changes from 1 to 2 (every 2 that follows directly after a 1)
decreasing ... where the list changes from 2 to 1 (every 1 that follows directly after a 2)
ones ... of all digits that are 1
twos ... of all digits that are 2
all ... all the digits
none ... none of the digits. 0 is fine if the list is 1-indexed. A negative number is fine if the list is 0-indexed. You may also output an empty list or string.

Test cases:
These are 1-indexed. You may choose if you want 1-indexed or 0-indexed. The same vectors are used for different strings in the test cases.
--------------------------------
Vector:
1 1 2 2 2 1 2 2 1 1 2

String       - Output
increasing   - 3, 7, 11
decreasing   - 6, 9
ones         - 1, 2, 6, 9, 10
twos         - 3, 4, 5, 7, 8, 11
all          - 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11
none         - 0 / []

------------------------------------
Vector:
1

String:
ones         - 1
all          - 1
decreasing / increasing / twos / none  - 0 / []

Scoring
As this is code-golf, the answer with the least bytes wins.
Explanations are encouraged!

So far none of the answers seem to output a list as shown in the example. (ie, joined by ", " with no trailing delimiter).  As the challenge text doesn't say how flexible the list can be, what's normally accepted for challenges like this?

It's normally very flexible. As long as it's a list of numbers you're fine.

JavaScript (Firefox 30-57), 74 73 bytes
(a,[s],i=0,p)=>[for(e of a)if({i:e>p,d:e<p,o:e<2,t:e>1,a:1}[p=e,i++,s])i]

Array comprehensions are a neat way of combining map and filter in one go. Edit: Saved 1 byte thanks to @edc65.

Haskell, 112 83 81 bytes
s%l=[i|(i,p,q)<-zip3[1..]l$l!!0:l,elem(s!!0,1<2)$zip"idota"[q<p,p<q,p<2,1<p,1<2]]

Try it online! Example usage: "increasing"%[1,1,2,1,2]. Results are 1-indexed.
Partly inspired by Lynn's Haskell answer.

Python 2, 136 131 119 108 97 bytes

Saved five bytes; using a lambda function.
Saved twelve bytes thanks to TFeld; golfing two conditions.
Saved eleven bytes thanks to Mr. Xcoder; using enumerate() instead of range(len()).
Saved eleven bytes by using a list instead of a dictionary and using 0-indexing (as in TFeld's answer) and golfing "adinot".find(m[0]) to ord(m[0])/3-32.

lambda l,m:[j for j,k in enumerate(l)if[1,j*k<j*l[~-j],0,j*k>j*l[~-j],0,k<2,k>1][ord(m[0])/3-32]]

Try it online!

Since the input is always 1or 2, you can change (l[j]>1)*(l[~-j]<2) to (l[j]>l[~-j])  for 119 bytes

Also, you can save a byte by switching to 0-indexed

@TFeld Thanks; though I think I will stick with 1-indexed.

108 bytes, using enumerate()

Python 2, 117 111 110 99 97 92 bytes
lambda l,t:[i for i,v in enumerate(l)if[l[i+i/~i]<v,0,v<2,v>1,1,l[i+i/~i]>v][ord(t[0])/3%7]]

Try it online!
0-indexed
Switched to using Jonathan's indexing, and golfed ord(m[0])/3-32 to ord(t[0])/3%7

You can golf l[i]==2 to l[i]>1.

MATL, 32 31 30 29  bytes
dQ~fQGqfOOGofGd1=fQGfO[]Xhjs)

Output is 1-based, or empty.
Try it online!
Explanation
The code computes the six possible outputs for the array input, and then selects the appropriate output depending on the string input.
To select the output, the ASCII code points of all characters of the string input are added. The result modulo 9 gives 6, 1, 5, 2, 7, 0 respectively for 'increasing', 'decreasing', 'ones', 'twos', 'all', 'none'. Since all the resulting numbers are distinct this can be used as a selection criterion.
Instead of actually performing a modulo 9 operation on the sum, the list of possible inputs is extended to 9 entries (some of which are dummy), and so indexing into that list is automatically done modulo 9.
d     % Implicit input: numeric vector. Push vector of consecutive differences.
      % Contains -1, 0 or 1
Q~    % For each entry: add 1, negate. This turns -1 into 1, other values into 0
f     % Push indices of nonzeros
Q     % Add 1 to each entry (compensates the fact that computing consecutive
      % differences removes one entry). This the output for 'decreasing'
Gq    % Push input again. Subtract 1 from the code points
f     % Push indices of nonzeros. This is the output for 'twos'
OO    % Push two zeros. These are used as placeholders
Go    % Push input and compute parity of each entry
f     % Push indices of nonzeros. This is the output for 'ones'
Gd    % Push input and compute consecutive differences
1=    % Test each entry for equality with 1
f     % Push indices of nonzeros
Q     % Add 1. This is the output for 'increasing'
Gf    % Push indices for all input (nonzero) entries. This is the output for 'all'
O     % Push zeros. Used as placeholder
[]    % Push empty array. This is the output for 'none'
Xh    % Concatenate stack into a cell array
j     % Input a string
s     % Sum of code points
)     % Use as an index into the cell aray. Implicitly display

Jelly, 27 bytes
>2\0;
NÇ
Ị
=2

ḟ
⁹Ḣ“hɠ»iµĿT

Try it online!
-3 thanks to Jonathan Allan.

Save three bytes by using the dictionary word "diota" - note that link 0 gets it right, but you could reorder again and use "antidote" or other such word and allow your test harness to work again.

@JonathanAllan I thought link 0 was the bottom-most link, but apparently it's like Ç but weirder, thanks! (also I just learned a new word :p)

J, 73 bytes
g=.[:I.[=0,2-/\]
(_1 g])`(1 g])`(1=])`(2=])`(i.@#@])`_1:@.('idotan'i.{.@[)

Would be curious to see how this can be significantly condensed -- I believe it can (10 chars just for all those agenda parens!)

g - helper verb for increasing and decreasing, which just amount to comparing the values of infix \ runs of size 2
The rest just grabs the first character from the "command" and executes the corresponding case using Agenda @.

Try it online!

Do 1=] and 2=] not work? Also, what if g took a number as its left argument and a list as its right argument and returned the indices where 2-/\  applied to the list equaled the left argument. That way you could pass it _1 or 1 to find decreasing and increasing instead of using an adverb.

@cole Good comments.  I made the changes, and the result is much cleaner, though 73 still seems like a high byte count.  I mean, J is tying the JS here.... the shame!

Python 2, 92 bytes
lambda a,s:[i for i,(x,y)in enumerate(zip([0]+a,a))if[0<x<y,0,y<2,y>1,1,x>y][ord(s[0])/3%7]]

Try it online!

Haskell, 91 bytes
(c:_)!l=[i|(i,y,x)<-zip3[1..]l$l!!0:l,c/='i'||x<y,c>'d'||x>y,c/='o'||y<2,c<'t'||y>1,c/='n']

Try it online!
Laikoni saved a byte.

You can save a byte with (i,y,x)<-zip3[1..]l$l!!0:l.

Some competition

Husk, 27 bytes
`fN!+mmëI=2ε¬moΘẊe><€¨Ÿȧö¨←

Try it online!
-9 thanks to H.PWiz.
I'm quite proud of this answer.

Golfed mostly by using ΘẊ> and ΘẊ< and \fN`

@H.PWiz how didn't I see those honestly

-1 byte A list indexed at 0 is the last element.

@H.PWiz Ooh I thought that the compressed string would be ¨₆Żσa¨ instead that's why I didn't use that feature, thanks. And now I can say it ties Jelly.

Jq 1.5, 131 bytes
Based on xcali's approach since string matching is shorter then my array version.
def D(s):[.[1]|gsub(" ";"")|match(s;"g").offset+(s|length)];./"
"|{i:D("12"),d:D("21"),o:D("1"),t:D("12"),a:D("."),n:[]}[.[0][0:1]]

Assumes jq is invoked with -Rs options and input appears on two lines e.g.
decreasing
1 1 2 2 2 1 2 2 1 1 2

Expanded:
def D(s): [
      .[1]                              # find where s appears
    | gsub(" ";"")                      # in the input and add
    | match(s;"g").offset + (s|length)  # length to get ending index
  ]
;

  ./"\n"                                # split on newline
| {i:D("12"),                           # increasing
   d:D("21"),                           # decreasing
   o:D("1"),                            # ones
   t:D("2"),                            # twos
   a:D("."),                            # all
   n:[]                                 # none
  }[.[0][0:1]]

Try it online!

Java (OpenJDK 8), 266 217 213 205 172 171 155 131 bytes
s->a->{int i=0,l=0,c=s.charAt(0)-97;for(int e:a){if(++i>1&(c==8&e>l|c==3&e<l)|c==14&(l=e)<2|c>18&l>1|c<1)System.out.print(i+",");}}

Try it online!

If you define y as a char, you can golf equality tests like y.equals("a") to y=='a', y==97 or even y<98.

@JonathanFrech Was just changing it :)

The TIO at least is not the output I would expect.  While only given by example, the list requires a space between elements and no trailing comma.

Since 19 is c's highest value, c==19 is equal to c>18.

15 bytes can be saved but using indexing from 1: for(;i<a.length;i++){if(i>0&(c==8&a[i]>l|c==3&a[i]<l))f=1;l=a[i]; can be replaced with for(int e:a){if(++i>1&(c==8&e>l|c==3&e<l))f=1;l=e;

131 bytes: s->a->{int i=0,l=0,c=s.charAt(0)-97;for(int e:a){if(++i>1&(c==8&e>l|c==3&e<l)|c==14&(l=e)<2|c>18&l>1|c<1)System.out.print(i+",");}}

Java 8, 233 229 216 bytes
l->s->{int i=s.charAt(0)-97,k=0,j=1;for(s=(l+"").replaceAll("[^12]","");s.length()*j>0;System.out.print(j++<0?"":(k+=j)+","),s=s.substring(j))j=i<1?0:s.indexOf(i<4?"21":i<9?"12":i<14?" ":i<15?"1":"2")+(i>2&i<9?1:0);}

This String approach ended up longer than I was expecting.. But even thought I'm hugely out-golfed by the other Java 8 answer, I decided to post it anyway.
It can definitely be golfed, even with this approach.. The "none" and "increase/decreasing" mainly caused some workaround that cost some bytes..
The result is 1-indexed.
Explanation:
Try it here.
l->s->{                          // Method with List and String parameters
  int i=s.charAt(0)-97,          //  First character of the String - 97
                                 //   (i=8; d=3; o=14; t=19; a=0; n=13)
      k=0,                       //  Total counter
      j=1;                       //  Index integer
  for(s=(l+"")                   //  toString of the List,
         .replaceAll("[^12]","");//   and leave only the 1s and 2s
      s.length()*j>0             //  Loop as long as `j` and the size of the String
                                 //  are both larger than 0
      ;                          //   After every iteration:
      System.out.print(          //    Print:
       j++<0?                    //     If `j` is -1:
        ""                       //      Print nothing
       :                         //     Else:
        (k+=j)+",")              //      Print the current index
      ,s=s.substring(j))         //    And then remove the part of the String we've checked
    j=i<1?                       //   If "all":
                                 //    Change `j` to 0
      :                          //   Else:
       s.indexOf(                //    Replace `j` with the next index of:
        i<1?                     //     If "all":
         s.charAt(0)+""          //      The next character
        :i<4?                    //     Else-if "decreasing":
         "21"                    //      Literal "21"
        :i<9?                    //     Else-if "increasing":
         "12"                    //      Literal "12"
        :i<14?                   //     Else-if "none":
         " "                     //      Literal space (any char that isn't present)
        :i<15?                   //     Else-if "one":
         "1"                     //      Literal "1"
        :                        //     Else(-if "two"):
         "2")                    //      Literal "2"
       +(i>2&i<9?1:0);           //     +1 if it's "increasing"/"decreasing"
                                 //  End of loop (implicit / single-line body)
}                                // End of method

Perl 5, 71 + 2 (-nl) = 73 bytes
$p=/l/?'.':/t/?2:/^o/?1:/d/?21:/i/?12:0;$_=<>;s/ //g;say pos while/$p/g

Try it online!
Revised logic is effectively the same as the below explanation, but the pattern matches have been shortened.
Previously:
$p=/all/?'.':/^o/?1:/^t/?2:/^d/?21:/^i/?12:0;$_=<>;s/ //g;say pos while/$p/g

Try it online!
Outputs nothing if the criteria is not matched.
Explained:
$p=          # set the pattern to seach based on the input string
  /all/?'.'  # any character
 :/^o/?1     # starts with 'o', find ones
 :/^t/?2     # starts with 't', find twos
 :/^d/?21    # starts with 'd', find decreasing
 :/^i/?12    # starts with 'i', find increasing
 :0;         # anything else: create pattern that won't match
$_=<>;s/ //g;# read the digits and remove spaces
say pos while/$p/g # output position(s) of all matches

source: Stack Exchange

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

sort: votes


text:
Primitive roots density of number
Definition:

A number m is called a primitive root of a prime p the condition that  the smallest integer k for which p dividies mk-1 is p-1

Your task
Given a tuple (a,b) of positive integers, return the fraction:
(number of primes p equal to or less than a which has b as a primitive root) divided by (number of primes equal to or less than a)
Test Cases
Assuming Artin's Conjecture to be true, giving (A very big number, 2) should return a value around .3739558136...
The challenge is for the fastest code, not necessarily the shortest one.
Timing
My crappy code takes 10 seconds for a million on my PC (intel i3 6th Gen, 8GB RAM, others I forgot), so your code should naturally beat that speed.
This is my first challenge. Feeback is appreciated. :)

Darn why there's no latex in CG SE :/

Type it here, and post it as images. That's what I did in this one.

Can you add some test cases, please?

https://codegolf.stackexchange.com/tags/fastest-code/info

You should specify how the code will be tested, by whom, and on what platform. Something like: "The program must be able to handle 1 million in less than 1 minute on my computer:
Specs: 4 CPUs, i5-4300U CPU @ 1.9 GHz, 7.5G of RAM. The program that finishes for 1 million the fastest wins." You need some way to determine the winner.

@StewieGriffin Yes, I should, but still I didn't because my desktop is sent away to be repaired, and now I'm working on the cheapest laptop of 2014, that too made by the stupidest company you can think of. I will update once I get my desktop back (after ~7 days, I think)

Why do you have a laptop made by Volkswagen???

"This is my first golf challenge" I see no golfing required here, as it's [tag:fastest-code]

C (gcc)
Around 0.6 sec for 1,000,000.
int modpow(long b,int e,long n){
	long r=1;
	while(e){
		if(e&1) r=r*b%n;
		b=b*b%n;
		e>>=1;
	}
	return r;
}
float f(int a,int b){
	int ln=1;
	for(int p=2;p<=a;p*=ln,ln++);
	int* primes = malloc((a+1)*(sizeof(int)));
	int** factors = malloc((a+1)*sizeof(int*));
	primes[0] = 0;
	primes[1] = 0;
	for(int i=2;i<=a;i++){
		primes[i] = 1;
		factors[i] = malloc(ln*sizeof(int));
	}
	factors[1] = malloc(sizeof(int));
	factors[1][1] = 0;
	for(int p=2;p*p<=a;p++){
		if(primes[p]){
			for(int j=p*2;j<=a;j+=p){
				primes[j] = 0;
				factors[j][0]++;
				factors[j][factors[j][0]] = p;
			}
		}
	}
	int count1 = 0;
	int count2 = 0;
	for(int p=2;p<=a;p++){
		if(!primes[p]) continue;
		count2++;
		int n=p-1;
		int m=p-1;
		int prim=1;
		for(int j=1;j<=factors[n][0];j++){
			int q=factors[n][j];
			if(modpow(b,n/q,p)==1){
				prim=0;
				break;
			}
			while(m%q==0){
				m/=q;
			}
		}
		if(m>1){
			if(modpow(b,n/m,p)==1){
				prim=0;
			}
		}
		count1 += prim;
	}
	return (float)count1/count2;
}

Try it online!

hey! +1 from me then!

@Jenny_mathy it's better now once I switch to C

C++11 + libop
1.23 sec on my slow laptop for 10,000,000.
#include <cstdint>
#include <vector>
#include <algorithm>
#include <iostream>
#include <utility>

#include "libop/op.h"

// Returns 2^-32 mod m, -m^(-1) mod 2^32
inline std::pair<uint64_t, uint64_t> mont_modinv32(uint64_t m) {
    uint64_t a = 1ull << 31;
    uint64_t u = 1;
    uint64_t v = 0;

    while (a > 0) {
        a = a >> 1;
        if ((u & 1) == 0) {
            u = u >> 1; v = v >> 1;
        } else {
            u = ((u ^ m) >> 1) + (u & m);
            v = (v >> 1) + (1ull << 31);
        }
    }

    return std::make_pair(u, v);
}

// Returns (ab)R mod n given aR mod n, bR mod n, n and -n^(-1) mod R, with R = 2^32
inline uint64_t montmul32(uint64_t a, uint64_t b, uint64_t n, uint64_t nneginv) {
    uint64_t T = a*b;
    uint32_t m = T*nneginv; // m = T*-n^(-1) (mod 2^32)
    uint64_t t = (T + m*n) >> 32;
    return t >= n ? t - n : t;
}

double f(uint32_t a, uint32_t b) {
    std::vector<uint32_t> primes;
    op::primes_below(a + 1, std::back_inserter(primes));

    int num_primitives = 0;

    for (auto p : primes) {
        if (p == 2) {
            num_primitives += b == 1;
            continue;
        }

        uint32_t s = p - 1;
        uint32_t pneginv = mont_modinv32(p).second;
        uint32_t montb = (uint64_t(b) << 32) % p;
        uint64_t mont1 = (1ull << 32) % p;

        uint32_t pows[32] = {montb};
        for (int i = 1; s >> i; ++i) {
            montb = montmul32(montb, montb, p, pneginv);
            pows[i] = montb;
        }

        bool primitive_root = true;
        for (auto& kv : op::factorization(s)) {
            uint32_t e = s / kv.first;

            uint64_t r = mont1;
            for (int i = 0; e; ++i) {
                if (e & 1) r = montmul32(r, pows[i], p, pneginv);
                e >>= 1;
            }

            if (r == mont1) {
                primitive_root = false;
                break;
            }
        }

        num_primitives += primitive_root;
    }

    return num_primitives / double(primes.size());
}

Mathematica
(t=0;
 f=PrimePi[#];
 d=#2;
 For[i=1,i<=f,i++,If[PrimitiveRoot[Prime[i],d]==d,t++]];
 N[t/f])&[1000000,2]//AbsoluteTiming

Try it online  Paste the code and press shift-enter
Takes 3.2 sec to find 1.000.000

This should have PrimitiveRoot[Prime[i],d]==d to work in full generality. Otherwise, given input b=3, it will not count a prime that has 3 as a primitive root if it also has 2 as a primitive root, because it will find 2 first.

@MishaLavrov if you see the edit history you'll see that this was my first approach but then I thought it wasn't necessary. I'll change it back. thanks!

@Jenny_mathy hey we're on the same order of magnitude :P

I believe that NextPrime might be a bit faster than Prime.

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


text:
(-a) × (-a) = a × a
We all know that \$(-a) \times (-a) = a \times a\$ (hopefully), but can you prove it?
Your task is to prove this fact using the ring axioms.  What are the ring axioms?  The ring axioms are a list of rules that two binary operations on a set have to follow.  The two operation are addition, \$+\$, and multiplication, \$\times\$.  For this challenge here are the ring axioms where \$+\$ and \$\times\$ are closed binary operations on some set \$S\$, \$-\$ is a closed unary operation on \$S\$, and \$a\$, \$b\$, \$c\$ are members of \$S\$:

\$a + (b + c) = (a + b) + c\$
\$a + 0 = a\$
\$a + (-a) = 0\$
\$a + b = b + a\$*
\$a \times (b \times c) = (a \times b) \times c\$
\$a \times 1 = a\$†
\$1 × a = a\$†
\$a \times (b + c) = (a \times b) + (a × c)\$
\$(b + c) \times a = (b \times a) + (c \times a)\$

Your proof should be a string of equalities each being the application of one axiom.
You may apply the axioms to either the entire expression or to some sub-expression.  For example if we have \$(a + c) + (b + c)\$ we can apply Axiom 4 to just the \$(b + c)\$ term, the \$(a + c)\$ term or the entire expression as a whole.  The variables can also stand in for arbitrarily complex expressions for instance we can apply axiom 4 to \$((a \times c) + b) + ((-a) + 1)\$ to get \$((-a) + 1) + ((a \times c) + b)\$.  In each step of the proof you can only apply one axiom to one expression.  All axioms are bidirectional, meaning substitution can go in either direction.  Things like the following are not allowed
(a + b) + (c + d) = (a + (b + c)) + d Ax. 1

This should be done in two steps:
(a + b) + (c + d) = ((a + b) + c) + d Ax. 1
                  = (a + (b + c)) + d Ax. 1

Facts you might normally take for granted but are not listed on the axioms list cannot be assumed, for example \$(-a) = (-1) \times a\$ is true but requires multiple steps to preform.
User Anthony has kindly provided a online proof validator
 that can be used as a replacement for TIO.
Example proof
Here is an example proof that \$-(-a) = a\$ with the axioms used labeled on the right of each step.
 -(-a) = (-(-a)) + 0          Ax. 2
       = 0 + (-(-a))          Ax. 4
       = (a + (-a)) + (-(-a)) Ax. 3
       = a + ((-a) + (-(-a))) Ax. 1
       = a + 0                Ax. 3
       = a                    Ax. 2

Try it online!
You will be tasked to prove \$(-a) \times (-a) = a \times a\$ using successive substitution like that shown above.
Scoring
This is proof-golf so your answers will be scored in number of steps taken to get from \$(-a) \times (-a)\$ to \$a \times a\$, with a lower score being better.
Lemmas
Some answers have chosen to use Lemmas in their proofs, so I will describe how that should be scored to avoid any confusion.  For the uninitiated, lemmas are proofs of facts that you use later in the proof.  In real mathematics they can be helpful in organizing your thoughts or conveying information clearly to the reader.  In this challenge using lemmas should not have an direct effect on your score.  (Although proof organization may make it easier or harder to golf)
If you choose to use lemmas it will cost as many steps as it took to prove that lemma in the first place each time you use it.  For example the here is the score breakdown of a proof using lemmas.
Lemma:
a × 0 = 0

Proof (7 steps):
a × 0 = (a × 0) + 0                        Ax. 2 (1)
      = (a × 0) + ((a × b) + (-(a × b)))   Ax. 3 (1)
      = ((a × 0) + (a × b)) + (-(a × b))   Ax. 1 (1)
      = (a × (0 + b)) + (-(a × b))         Ax. 8 (1)
      = (a × (b + 0)) + (-(a × b))         Ax. 4 (1)
      = (a × b) + (-(a × b))               Ax. 2 (1)
      = 0                                  Ax. 3 (1)

Theorem:
(a × 0) + (b × 0) = 0

Proof (15 steps):
(a × 0) + (b × 0) = 0 + (b × 0)  Lemma (7)
                  = (b × 0) + 0  Ax. 4 (1)
                  = b × 0        Ax. 2 (1)
                  = 0            Lemma (7)

*: It has been pointed out that this axiom is not strictly necessary to prove this property, however you are still allowed to use it.
†: Since \$1\$ does not appear in the desired equality any proof that uses these axioms is not minimal.  That is these axioms cannot help with proving the desired fact.  They have been included just for the sake of completeness.

Is a program we write supposed to solve this, or just print the answer?

@Tahg You're supposed to prove it and submit your proof as an answer. This is different from most (if not all) problems you will see here.

I got frustratingly close before I realized that a*0=0 isn't in the list of axioms.

@sparr That can be proven from the axioms, though: a0 + 0 = a0 = a*(0 + 0) = a0 + a0 <=> a0 + 0 + (-(a0)) = a0 + a0 + (-(a0)) <=> 0 = a0

Erm... I might be wrong but isn't this way off-topic? Shouldn't answers contain code?

@icrieverytim if it helps, think of the axiom list as a programming language with nine built-in parameter substitution functions, and this is a code golf for a function that turns a specific input into a specific output.

@icrieverytim Meta post

Maybe I'm missing something obvious here, but why are axioms 6 and 7 even there? There isn't any 1 = ... to use them with. (Also, none of the answers seem to use them.) Could you give any example where 6 and/or 7 could be used for a some steps?

@KevinCruijssen 6 and 7 are not useful for this problem but they are ring axioms.  I didn't see any harm in adding 2 axioms that couldn't be used for the sake of completion.

@SriotchilismO'Zaic Ah ok, I didn't realize those are all ring axioms for $+$ and $×$. I thought it was just a subset only usable by the challenge.

Note that it's possible to derive a+b=b+a from the other axioms, for example at http://us.metamath.org/mpeuni/addcom.html (tl;dr a+b+a+b=2(a+b)=2a+2b=a+a+b+b and using -a and -b b+a=a+b)

@CalculatorFeline There is already a note pointing that out :)

The post says "to prove this property", which is more specific than "to prove anything".

I think I proved 18 is optimal: https://pastebin.com/raw/DieBKpA1

@StackMeter  That is really more of an outline than an actual proof.  The first step where you assert that there are only two ways to do it is at least dubious to me.  You would need to show that.  And if you did the rest of the proof would still need to hold up to scrutiny.  The underlying ideas here might be valid but it is hard to tell at the moment.

@Wheat Wizard I'll change the wording to reflect that

18 Steps
(-a)*(-a) = ((-a)*(-a))+0                                             Axiom 2
          = ((-a)*(-a))+(((a*a)+(a*(-a)))+(-((a*a)+(a*(-a)))))        Axiom 3
          = (((-a)*(-a))+((a*a)+(a*(-a))))+(-((a*a)+(a*(-a))))        Axiom 1
          = (((a*a)+(a*(-a)))+((-a)*(-a)))+(-((a*a)+(a*(-a))))        Axiom 4
          = ((a*a)+((a*(-a))+((-a)*(-a))))+(-((a*a)+(a*(-a))))        Axiom 1
          = ((a*a)+((a+(-a))*(-a)))+(-((a*a)+(a*(-a))))               Axiom 9
          = ((a*a)+(0*(-a)))+(-((a*a)+(a*(-a))))                      Axiom 3
          = ((a*(a+0))+(0*(-a)))+(-((a*a)+(a*(-a))))                  Axiom 2
          = ((a*(a+(a+(-a))))+(0*(-a)))+(-((a*a)+(a*(-a))))           Axiom 3
          = (((a*a)+(a*(a+(-a))))+(0*(-a)))+(-((a*a)+(a*(-a))))       Axiom 8
          = ((a*a)+((a*(a+(-a)))+(0*(-a))))+(-((a*a)+(a*(-a))))       Axiom 1
          = (a*a)+(((a*(a+(-a)))+(0*(-a)))+(-((a*a)+(a*(-a)))))       Axiom 1
          = (a*a)+((((a*a)+(a*(-a)))+(0*(-a)))+(-((a*a)+(a*(-a)))))   Axiom 8
          = (a*a)+(((a*a)+((a*(-a))+(0*(-a))))+(-((a*a)+(a*(-a)))))   Axiom 1
          = (a*a)+(((a*a)+((a+0)*(-a)))+(-((a*a)+(a*(-a)))))          Axiom 9
          = (a*a)+(((a*a)+(a*(-a)))+(-((a*a)+(a*(-a)))))              Axiom 2
          = (a*a)+0                                                   Axiom 3
          = a*a                                                       Axiom 2

I wrote a program to check my solution. So if you find an error in this, then my program is wrong too.

@Etoplay Just out of curiosity, did you write your program in Prolog?

It would be great if you could include your program.  It could certainly help verify other solutions.

How did you get from the first line to the second just by applying one axiom one time?

@SztupY Axiom 3 is v + (-v) = 0 let v =  ((a*a)+(a*(-a)) and you get there in 1 step.

ah, cool. It was a bit hard to see

validated

18 steps
Different from the already posted 18-step solution.
a*a = a*a + 0                                                 A2
    = a*a + ((a*(-a) + a*(-a)) + (-(a*(-a) + a*(-a))))        A3
    = (a*a + (a*(-a) + a*(-a))) + (-(a*(-a) + a*(-a)))        A1
    = (a*a + a*((-a) + (-a))) + (-(a*(-a) + a*(-a)))          A8
    = a*(a + ((-a) + (-a))) + (-(a*(-a) + a*(-a)))            A8
    = a*((a + (-a)) + (-a)) + (-(a*(-a) + a*(-a)))            A1
    = a*(0 + (-a)) + (-(a*(-a) + a*(-a)))                     A3
    = a*((-a) + 0) + (-(a*(-a) + a*(-a)))                     A4
    = a*(-a) + (-(a*(-a) + a*(-a)))                           A2
    = (a + 0)*(-a) + (-(a*(-a) + a*(-a)))                     A2
    = (a + (a + (-a)))*(-a) + (-(a*(-a) + a*(-a)))            A3
    = ((a + a) + (-a))*(-a) + (-(a*(-a) + a*(-a)))            A1
    = ((-a) + (a + a))*(-a) + (-(a*(-a) + a*(-a)))            A4
    = ((-a)*(-a) + (a + a)*(-a)) + (-(a*(-a) + a*(-a)))       A9
    = ((-a)*(-a) + (a*(-a) + a*(-a))) + (-(a*(-a) + a*(-a)))  A9
    = (-a)*(-a) + ((a*(-a) + a*(-a)) + (-(a*(-a) + a*(-a))))  A1
    = (-a)*(-a) + 0                                           A3
    = (-a)*(-a)                                               A2

Interesting to see someone do it backwards.  All the steps are reversible so this is a fine proof.

That it goes upside down is mostly accidental. The proof is actually fairly symmetric: I use two similar sequences of steps to get from either end to the middle term a*(-a) + stuff.

validated

29 26 Steps
No lemmas!
Comment if you see anything wrong. (It's very easy to make a mistake)
(-a) × (-a) = ((-a) + 0) × (-a)                                                  Ax. 2
            = ((-a) + (a + (-a))) × (-a)                                         Ax. 3
            = ((a + (-a)) + (-a)) × (-a)                                         Ax. 4
            = (a + ((-a) + (-a))) × (-a)                                         Ax. 1
            = (a × (-a)) + (((-a) + (-a)) × (-a))                                Ax. 9
            = (a × ((-a) + 0)) + (((-a) + (-a)) × (-a))                          Ax. 2
            = (a × ((-a) + (a + (-a)))) + (((-a) + (-a)) × (-a))                 Ax. 3
            = (a × ((a + (-a)) + (-a))) + (((-a) + (-a)) × (-a))                 Ax. 4
            = (a × (a + ((-a) + (-a)))) + (((-a) + (-a)) × (-a))                 Ax. 1
            = ((a × a) + (a × ((-a) + (-a)))) + (((-a) + (-a)) × (-a))           Ax. 8
            = (a × a) + ((a × ((-a) + (-a))) + (((-a) + (-a)) × (-a)))           Ax. 1
            = (a × a) + (((a × (-a)) + (a × (-a))) + (((-a) + (-a)) × (-a)))     Ax. 8
            = (a × a) + (((a + a) × (-a)) + (((-a) + (-a)) × (-a)))              Ax. 9
            = (a × a) + (((a + a) + ((-a) + (-a))) × (-a))                       Ax. 9
            = (a × a) + ((((a + a) + (-a)) + (-a)) × (-a))                       Ax. 1
            = (a × a) + (((a + (a + (-a))) + (-a)) × (-a))                       Ax. 1
            = (a × a) + (((a + 0) + (-a)) × (-a))                                Ax. 3
            = (a × a) + ((a + (-a)) × (-a))                                      Ax. 2
            = (a × a) + (0 × (-a))                                               Ax. 3
            = (a × a) + ((0 × (-a)) + 0)                                         Ax. 2
            = (a × a) + ((0 × (-a)) + ((0 × (-a)) + (-(0 × (-a)))))              Ax. 3
            = (a × a) + (((0 × (-a)) + (0 × (-a))) + (-(0 × (-a))))              Ax. 1
            = (a × a) + (((0 + 0) × (-a)) + (-(0 × (-a))))                       Ax. 9
            = (a × a) + ((0 × (-a)) + (-(0 × (-a))))                             Ax. 2
            = (a × a) + 0                                                        Ax. 3
            = (a × a)                                                            Ax. 2

Credit goes to Maltysen for 0 × (-a) = 0

validated

18 steps
Not the first 18-step proof, but it’s simpler than the others.
(-a)*(-a)
= (-a)*(-a) + 0                             [Axiom 2]
= (-a)*(-a) + ((-a)*a + -((-a)*a))          [Axiom 3]
= ((-a)*(-a) + (-a)*a) + -((-a)*a)          [Axiom 1]
= ((-a)*(-a) + ((-a) + 0)*a) + -((-a)*a)    [Axiom 2]
= ((-a)*(-a) + ((-a)*a + 0*a)) + -((-a)*a)  [Axiom 9]
= (((-a)*(-a) + (-a)*a) + 0*a) + -((-a)*a)  [Axiom 1]
= ((-a)*((-a) + a) + 0*a) + -((-a)*a)       [Axiom 8]
= ((-a)*(a + (-a)) + 0*a) + -((-a)*a)       [Axiom 4]
= ((-a)*0 + 0*a) + -((-a)*a)                [Axiom 3]
= (0*a + (-a)*0) + -((-a)*a)                [Axiom 4]
= ((a + (-a))*a + (-a)*0) + -((-a)*a)       [Axiom 3]
= ((a*a + (-a)*a) + (-a)*0) + -((-a)*a)     [Axiom 9]
= (a*a + ((-a)*a + (-a)*0)) + -((-a)*a)     [Axiom 1]
= (a*a + (-a)*(a + 0)) + -((-a)*a)          [Axiom 8]
= (a*a + (-a)*a) + -((-a)*a)                [Axiom 2]
= a*a + ((-a)*a + -((-a)*a))                [Axiom 1]
= a*a + 0                                   [Axiom 3]
= a*a                                       [Axiom 2]

Validate

23 steps
(-a) * (-a) = ((-a) * (-a)) + 0                                 ✔ axiom 2
            = ((-a) * (-a)) + (((-a) * a) + -((-a) * a))        ✔ axiom 3
            = (((-a) * (-a)) + (-a) * a) + -((-a) * a)          ✔ axiom 1
            = (-a) * (-a + a) + -((-a) * a)                     ✔ axiom 8
            = (-a) * (a + (-a)) + -((-a) * a)                   ✔ axiom 4
            = ((-a) * 0) + -((-a) * a)                          ✔ axiom 3
            = (((-a) * 0) + 0) + -((-a) * a)                    ✔ axiom 2
            = ((-a) * 0 + ((-a)*0 + -((-a)*0))) + -((-a) * a)   ✔ axiom 3
            = (((-a) * 0 + (-a)*0) + -((-a)*0)) + -((-a) * a)   ✔ axiom 1
            = ((-a) * (0 + 0) + -((-a)*0)) + -((-a) * a)        ✔ axiom 8
            = ((-a) * 0 + -((-a)*0)) + -((-a) * a)              ✔ axiom 2
            = 0 + -((-a) * a)                                   ✔ axiom 3
            = (0* a) + -(0*a) + -((-a) * a)                     ✔ axiom 3
            = ((0+0)* a) + -(0*a) + -((-a) * a)                 ✔ axiom 2
            = ((0 * a ) + (0*a) + -(0*a)) + -((-a) * a)         ✔ axiom 9
            = ((0 * a ) + ((0*a) + -(0*a))) + -((-a) * a)       ✔ axiom 1
            = ((0 * a ) + 0) + -((-a) * a)                      ✔ axiom 3
            = (0 * a ) + -((-a) * a)                            ✔ axiom 2
            = ((a + -a) * a ) + -((-a) * a)                     ✔ axiom 3
            = ((a * a) + (-a) * a) + -((-a) * a)                ✔ axiom 9
            = (a * a) + (((-a) * a) + -((-a) * a))              ✔ axiom 1
            = (a * a) + 0                                       ✔ axiom 3
            = a * a                                             ✔ axiom 2

Try it online!
Yes you read that right, I've written a proof-checker for this puzzle (naturally there's a possibility that the checker itself is wrong)

Here’s a modest reward for the proof checker.

@EmilJeřábek wow, thank you!  Yeah, interesting trick with parse trees that, and not too painful to implement.  I have enjoyed playing a little with a fully general prover (Metamath) since.

A2: (-a) x (-a) = ((-a) + 0) x (-a)
A3:             = ((-a) + (a + (-a))) x (-a)
A9:             = ((-a) x (-a)) + ((a + (-a)) x (-a))
A4:             = ((-a) x (-a)) + (((-a) + a) x (-a))
A9:             = ((-a) x (-a)) + (((-a) x (-a)) + (a x (-a)))
A1:             = (((-a) x (-a)) + ((-a) x (-a))) + (a x (-a))
A2:             = (((-a) x (-a)) + ((-a) x (-a))) + (a x ((-a) + 0))
A3:             = (((-a) x (-a)) + ((-a) x (-a))) + (a x ((-a) + (a + (-a))))
A8:             = (((-a) x (-a)) + ((-a) x (-a))) + ((a x (-a)) + (a x (a + (-a))))
A8:             = (((-a) x (-a)) + ((-a) x (-a))) + ((a x (-a)) + ((a x a) + (a x (-a))))
A4:             = (((-a) x (-a)) + ((-a) x (-a))) + ((a x (-a)) + ((a x (-a)) + (a x a)))
A1:             = (((-a) x (-a)) + ((-a) x (-a))) + (((a x (-a)) + (a x (-a))) + (a x a))
A8:             = ((-a) x ((-a) + (-a))) + (((a x (-a)) + (a x (-a))) + (a x a))
A8:             = ((-a) x ((-a) + (-a))) + ((a x ((-a) + (-a))) + (a x a))
A1:             = (((-a) x ((-a) + (-a))) + (a x ((-a) + (-a)))) + (a x a)
A9:             = (((-a) + a) x ((-a) + (-a))) + (a x a)
A4:             = ((a + (-a)) x ((-a) + (-a))) + (a x a)
Lemma:          = (0 x ((-a) + (-a))) + (a x a)
A3:             = 0 + (a x a)
A4:             = (a x a) + 0
A2:             = (a x a)

Lemma: 0 = 0 x a

A3: 0 = (0 x a) + (-(0 x a))
A2:   = ((0 + 0) x a) + (-(0 x a))
A9:   = ((0 x a) + (0 x a)) + (-(0 x a))
A1:   = (0 x a) + ((0 x a) + (-(0 x a)))
A3:   = (0 x a) + 0
A2:   = (0 x a)

27 26 steps
Thank you Funky Computer Man for noticing a duplicate line.

Welcome to the site! I'm not sure why you create a lemma only to use it once but I suppose its not against the rules.

@FunkyComputerMan Thank you! You're right; I'm not sure what I was thinking when I wrote that lemma ^^. And thank you for your edit and your remark.

@JalilCompaoré I think you might be able to save that last A3 by starting by applying A2 to the second (-a) rather than the first. I'm not sure though, as I don't have the time to work through it right now.

304 steps
Community wiki because this proof is generated by Mathematica's FindEquationalProof function.
The proof is rather long. Mathematica doesn't know how to golf it.
This is the Mathematica code that generates the proof (requires Mathematica 11.3), where p, t, n means +, ×, - respectively:
ringAxioms = {ForAll[{a, b, c}, p[a, p[b, c]] == p[p[a, b], c]],
   ForAll[a, p[a, 0] == a],
   ForAll[a, p[a, n[a]] == 0],
   ForAll[{a, b}, p[a, b] == p[b, a]],
   ForAll[{a, b, c}, t[a, t[b, c]] == t[t[a, b], c]],
   ForAll[a, t[a, 1] == a], ForAll[a, t[1, a] == a],
   ForAll[{a, b, c}, t[a, p[b, c]] == p[t[a, b], t[a, c]]],
   ForAll[{a, b, c}, t[p[b, c], a] == p[t[b, a], t[c, a]]]};

proof = FindEquationalProof[t[n[a], n[a]] == t[a, a], ringAxioms];

proof["ProofNotebook"]

It is not easy to count the steps directly, so I calculate it by the number of paths from the axioms to the conclusion in the "proof graph".
graph = proof["ProofGraph"];
score = Sum[
  Length[FindPath[graph, axiom, "Conclusion 1", Infinity,
    All]], {axiom,
   Select[VertexList[graph], StringMatchQ["Axiom " ~~ __]]}]

Try it online!
This is the proof generated by the code:
Axiom 1

We are given that:

x1==p[x1, 0]

Axiom 2

We are given that:

x1==t[x1, 1]

Axiom 3

We are given that:

x1==t[1, x1]

Axiom 4

We are given that:

p[x1, x2]==p[x2, x1]

Axiom 5

We are given that:

p[x1, p[x2, x3]]==p[p[x1, x2], x3]

Axiom 6

We are given that:

p[x1, n[x1]]==0

Axiom 7

We are given that:

p[t[x1, x2], t[x3, x2]]==t[p[x1, x3], x2]

Axiom 8

We are given that:

p[t[x1, x2], t[x1, x3]]==t[x1, p[x2, x3]]

Axiom 9

We are given that:

t[x1, t[x2, x3]]==t[t[x1, x2], x3]

Hypothesis 1

We would like to show that:

t[n[a], n[a]]==t[a, a]

Critical Pair Lemma 1

The following expressions are equivalent:

p[0, x1]==x1

Proof

Note that the input for the rule:

p[x1_, x2_]\[TwoWayRule]p[x2_, x1_]

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, 0]->x1

where these rules follow from Axiom 4 and Axiom 1 respectively.

Critical Pair Lemma 2

The following expressions are equivalent:

p[x1, p[n[x1], x2]]==p[0, x2]

Proof

Note that the input for the rule:

p[p[x1_, x2_], x3_]->p[x1, p[x2, x3]]

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, n[x1_]]->0

where these rules follow from Axiom 5 and Axiom 6 respectively.

Critical Pair Lemma 3

The following expressions are equivalent:

t[p[1, x1], x2]==p[x2, t[x1, x2]]

Proof

Note that the input for the rule:

p[t[x1_, x2_], t[x3_, x2_]]->t[p[x1, x3], x2]

contains a subpattern of the form:

t[x1_, x2_]

which can be unified with the input for the rule:

t[1, x1_]->x1

where these rules follow from Axiom 7 and Axiom 3 respectively.

Critical Pair Lemma 4

The following expressions are equivalent:

t[x1, p[1, x2]]==p[x1, t[x1, x2]]

Proof

Note that the input for the rule:

p[t[x1_, x2_], t[x1_, x3_]]->t[x1, p[x2, x3]]

contains a subpattern of the form:

t[x1_, x2_]

which can be unified with the input for the rule:

t[x1_, 1]->x1

where these rules follow from Axiom 8 and Axiom 2 respectively.

Critical Pair Lemma 5

The following expressions are equivalent:

t[p[1, x1], 0]==t[x1, 0]

Proof

Note that the input for the rule:

p[x1_, t[x2_, x1_]]->t[p[1, x2], x1]

contains a subpattern of the form:

p[x1_, t[x2_, x1_]]

which can be unified with the input for the rule:

p[0, x1_]->x1

where these rules follow from Critical Pair Lemma 3 and Critical Pair Lemma 1 respectively.

Critical Pair Lemma 6

The following expressions are equivalent:

t[0, 0]==t[1, 0]

Proof

Note that the input for the rule:

t[p[1, x1_], 0]->t[x1, 0]

contains a subpattern of the form:

p[1, x1_]

which can be unified with the input for the rule:

p[x1_, 0]->x1

where these rules follow from Critical Pair Lemma 5 and Axiom 1 respectively.

Substitution Lemma 1

It can be shown that:

t[0, 0]==0

Proof

We start by taking Critical Pair Lemma 6, and apply the substitution:

t[1, x1_]->x1

which follows from Axiom 3.

Critical Pair Lemma 7

The following expressions are equivalent:

t[x1, 0]==t[p[x1, 1], 0]

Proof

Note that the input for the rule:

t[p[1, x1_], 0]->t[x1, 0]

contains a subpattern of the form:

p[1, x1_]

which can be unified with the input for the rule:

p[x1_, x2_]\[TwoWayRule]p[x2_, x1_]

where these rules follow from Critical Pair Lemma 5 and Axiom 4 respectively.

Critical Pair Lemma 8

The following expressions are equivalent:

t[0, p[1, x1]]==t[0, x1]

Proof

Note that the input for the rule:

p[x1_, t[x1_, x2_]]->t[x1, p[1, x2]]

contains a subpattern of the form:

p[x1_, t[x1_, x2_]]

which can be unified with the input for the rule:

p[0, x1_]->x1

where these rules follow from Critical Pair Lemma 4 and Critical Pair Lemma 1 respectively.

Critical Pair Lemma 9

The following expressions are equivalent:

t[p[x1, 1], p[1, 0]]==p[p[x1, 1], t[x1, 0]]

Proof

Note that the input for the rule:

p[x1_, t[x1_, x2_]]->t[x1, p[1, x2]]

contains a subpattern of the form:

t[x1_, x2_]

which can be unified with the input for the rule:

t[p[x1_, 1], 0]->t[x1, 0]

where these rules follow from Critical Pair Lemma 4 and Critical Pair Lemma 7 respectively.

Substitution Lemma 2

It can be shown that:

t[p[x1, 1], 1]==p[p[x1, 1], t[x1, 0]]

Proof

We start by taking Critical Pair Lemma 9, and apply the substitution:

p[x1_, 0]->x1

which follows from Axiom 1.

Substitution Lemma 3

It can be shown that:

p[x1, 1]==p[p[x1, 1], t[x1, 0]]

Proof

We start by taking Substitution Lemma 2, and apply the substitution:

t[x1_, 1]->x1

which follows from Axiom 2.

Substitution Lemma 4

It can be shown that:

p[x1, 1]==p[x1, p[1, t[x1, 0]]]

Proof

We start by taking Substitution Lemma 3, and apply the substitution:

p[p[x1_, x2_], x3_]->p[x1, p[x2, x3]]

which follows from Axiom 5.

Critical Pair Lemma 10

The following expressions are equivalent:

t[0, x1]==t[0, p[x1, 1]]

Proof

Note that the input for the rule:

t[0, p[1, x1_]]->t[0, x1]

contains a subpattern of the form:

p[1, x1_]

which can be unified with the input for the rule:

p[x1_, x2_]\[TwoWayRule]p[x2_, x1_]

where these rules follow from Critical Pair Lemma 8 and Axiom 4 respectively.

Critical Pair Lemma 11

The following expressions are equivalent:

t[p[1, 0], p[x1, 1]]==p[p[x1, 1], t[0, x1]]

Proof

Note that the input for the rule:

p[x1_, t[x2_, x1_]]->t[p[1, x2], x1]

contains a subpattern of the form:

t[x2_, x1_]

which can be unified with the input for the rule:

t[0, p[x1_, 1]]->t[0, x1]

where these rules follow from Critical Pair Lemma 3 and Critical Pair Lemma 10 respectively.

Substitution Lemma 5

It can be shown that:

t[1, p[x1, 1]]==p[p[x1, 1], t[0, x1]]

Proof

We start by taking Critical Pair Lemma 11, and apply the substitution:

p[x1_, 0]->x1

which follows from Axiom 1.

Substitution Lemma 6

It can be shown that:

p[x1, 1]==p[p[x1, 1], t[0, x1]]

Proof

We start by taking Substitution Lemma 5, and apply the substitution:

t[1, x1_]->x1

which follows from Axiom 3.

Substitution Lemma 7

It can be shown that:

p[x1, 1]==p[x1, p[1, t[0, x1]]]

Proof

We start by taking Substitution Lemma 6, and apply the substitution:

p[p[x1_, x2_], x3_]->p[x1, p[x2, x3]]

which follows from Axiom 5.

Substitution Lemma 8

It can be shown that:

p[x1, p[n[x1], x2]]==x2

Proof

We start by taking Critical Pair Lemma 2, and apply the substitution:

p[0, x1_]->x1

which follows from Critical Pair Lemma 1.

Critical Pair Lemma 12

The following expressions are equivalent:

n[n[x1]]==p[x1, 0]

Proof

Note that the input for the rule:

p[x1_, p[n[x1_], x2_]]->x2

contains a subpattern of the form:

p[n[x1_], x2_]

which can be unified with the input for the rule:

p[x1_, n[x1_]]->0

where these rules follow from Substitution Lemma 8 and Axiom 6 respectively.

Substitution Lemma 9

It can be shown that:

n[n[x1]]==x1

Proof

We start by taking Critical Pair Lemma 12, and apply the substitution:

p[x1_, 0]->x1

which follows from Axiom 1.

Critical Pair Lemma 13

The following expressions are equivalent:

x1==p[n[x2], p[x2, x1]]

Proof

Note that the input for the rule:

p[x1_, p[n[x1_], x2_]]->x2

contains a subpattern of the form:

n[x1_]

which can be unified with the input for the rule:

n[n[x1_]]->x1

where these rules follow from Substitution Lemma 8 and Substitution Lemma 9 respectively.

Critical Pair Lemma 14

The following expressions are equivalent:

t[x1, x2]==p[n[x2], t[p[1, x1], x2]]

Proof

Note that the input for the rule:

p[n[x1_], p[x1_, x2_]]->x2

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, t[x2_, x1_]]->t[p[1, x2], x1]

where these rules follow from Critical Pair Lemma 13 and Critical Pair Lemma 3 respectively.

Critical Pair Lemma 15

The following expressions are equivalent:

t[x1, x2]==p[n[x1], t[x1, p[1, x2]]]

Proof

Note that the input for the rule:

p[n[x1_], p[x1_, x2_]]->x2

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, t[x1_, x2_]]->t[x1, p[1, x2]]

where these rules follow from Critical Pair Lemma 13 and Critical Pair Lemma 4 respectively.

Critical Pair Lemma 16

The following expressions are equivalent:

p[1, t[x1, 0]]==p[n[x1], p[x1, 1]]

Proof

Note that the input for the rule:

p[n[x1_], p[x1_, x2_]]->x2

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, p[1, t[x1_, 0]]]->p[x1, 1]

where these rules follow from Critical Pair Lemma 13 and Substitution Lemma 4 respectively.

Substitution Lemma 10

It can be shown that:

p[1, t[x1, 0]]==1

Proof

We start by taking Critical Pair Lemma 16, and apply the substitution:

p[n[x1_], p[x1_, x2_]]->x2

which follows from Critical Pair Lemma 13.

Critical Pair Lemma 17

The following expressions are equivalent:

t[t[x1, 0], 0]==t[1, 0]

Proof

Note that the input for the rule:

t[p[1, x1_], 0]->t[x1, 0]

contains a subpattern of the form:

p[1, x1_]

which can be unified with the input for the rule:

p[1, t[x1_, 0]]->1

where these rules follow from Critical Pair Lemma 5 and Substitution Lemma 10 respectively.

Substitution Lemma 11

It can be shown that:

t[x1, t[0, 0]]==t[1, 0]

Proof

We start by taking Critical Pair Lemma 17, and apply the substitution:

t[t[x1_, x2_], x3_]->t[x1, t[x2, x3]]

which follows from Axiom 9.

Substitution Lemma 12

It can be shown that:

t[x1, 0]==t[1, 0]

Proof

We start by taking Substitution Lemma 11, and apply the substitution:

t[0, 0]->0

which follows from Substitution Lemma 1.

Substitution Lemma 13

It can be shown that:

t[x1, 0]==0

Proof

We start by taking Substitution Lemma 12, and apply the substitution:

t[1, x1_]->x1

which follows from Axiom 3.

Critical Pair Lemma 18

The following expressions are equivalent:

t[x1, t[0, x2]]==t[0, x2]

Proof

Note that the input for the rule:

t[t[x1_, x2_], x3_]->t[x1, t[x2, x3]]

contains a subpattern of the form:

t[x1_, x2_]

which can be unified with the input for the rule:

t[x1_, 0]->0

where these rules follow from Axiom 9 and Substitution Lemma 13 respectively.

Critical Pair Lemma 19

The following expressions are equivalent:

p[1, t[0, x1]]==p[n[x1], p[x1, 1]]

Proof

Note that the input for the rule:

p[n[x1_], p[x1_, x2_]]->x2

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, p[1, t[0, x1_]]]->p[x1, 1]

where these rules follow from Critical Pair Lemma 13 and Substitution Lemma 7 respectively.

Substitution Lemma 14

It can be shown that:

p[1, t[0, x1]]==1

Proof

We start by taking Critical Pair Lemma 19, and apply the substitution:

p[n[x1_], p[x1_, x2_]]->x2

which follows from Critical Pair Lemma 13.

Critical Pair Lemma 20

The following expressions are equivalent:

t[0, t[0, x1]]==t[0, 1]

Proof

Note that the input for the rule:

t[0, p[1, x1_]]->t[0, x1]

contains a subpattern of the form:

p[1, x1_]

which can be unified with the input for the rule:

p[1, t[0, x1_]]->1

where these rules follow from Critical Pair Lemma 8 and Substitution Lemma 14 respectively.

Substitution Lemma 15

It can be shown that:

t[0, x1]==t[0, 1]

Proof

We start by taking Critical Pair Lemma 20, and apply the substitution:

t[x1_, t[0, x2_]]->t[0, x2]

which follows from Critical Pair Lemma 18.

Substitution Lemma 16

It can be shown that:

t[0, x1]==0

Proof

We start by taking Substitution Lemma 15, and apply the substitution:

t[x1_, 1]->x1

which follows from Axiom 2.

Critical Pair Lemma 21

The following expressions are equivalent:

t[n[1], x1]==p[n[x1], t[0, x1]]

Proof

Note that the input for the rule:

p[n[x1_], t[p[1, x2_], x1_]]->t[x2, x1]

contains a subpattern of the form:

p[1, x2_]

which can be unified with the input for the rule:

p[x1_, n[x1_]]->0

where these rules follow from Critical Pair Lemma 14 and Axiom 6 respectively.

Substitution Lemma 17

It can be shown that:

t[n[1], x1]==p[n[x1], 0]

Proof

We start by taking Critical Pair Lemma 21, and apply the substitution:

t[0, x1_]->0

which follows from Substitution Lemma 16.

Substitution Lemma 18

It can be shown that:

t[n[1], x1]==n[x1]

Proof

We start by taking Substitution Lemma 17, and apply the substitution:

p[x1_, 0]->x1

which follows from Axiom 1.

Critical Pair Lemma 22

The following expressions are equivalent:

t[n[1], t[x1, x2]]==t[n[x1], x2]

Proof

Note that the input for the rule:

t[t[x1_, x2_], x3_]->t[x1, t[x2, x3]]

contains a subpattern of the form:

t[x1_, x2_]

which can be unified with the input for the rule:

t[n[1], x1_]->n[x1]

where these rules follow from Axiom 9 and Substitution Lemma 18 respectively.

Substitution Lemma 19

It can be shown that:

n[t[x1, x2]]==t[n[x1], x2]

Proof

We start by taking Critical Pair Lemma 22, and apply the substitution:

t[n[1], x1_]->n[x1]

which follows from Substitution Lemma 18.

Critical Pair Lemma 23

The following expressions are equivalent:

t[x1, n[1]]==p[n[x1], t[x1, 0]]

Proof

Note that the input for the rule:

p[n[x1_], t[x1_, p[1, x2_]]]->t[x1, x2]

contains a subpattern of the form:

p[1, x2_]

which can be unified with the input for the rule:

p[x1_, n[x1_]]->0

where these rules follow from Critical Pair Lemma 15 and Axiom 6 respectively.

Substitution Lemma 20

It can be shown that:

t[x1, n[1]]==p[n[x1], 0]

Proof

We start by taking Critical Pair Lemma 23, and apply the substitution:

t[x1_, 0]->0

which follows from Substitution Lemma 13.

Substitution Lemma 21

It can be shown that:

t[x1, n[1]]==n[x1]

Proof

We start by taking Substitution Lemma 20, and apply the substitution:

p[x1_, 0]->x1

which follows from Axiom 1.

Critical Pair Lemma 24

The following expressions are equivalent:

n[t[x1, x2]]==t[x1, t[x2, n[1]]]

Proof

Note that the input for the rule:

t[x1_, n[1]]->n[x1]

contains a subpattern of the form:

t[x1_, n[1]]

which can be unified with the input for the rule:

t[t[x1_, x2_], x3_]->t[x1, t[x2, x3]]

where these rules follow from Substitution Lemma 21 and Axiom 9 respectively.

Substitution Lemma 22

It can be shown that:

t[n[x1], x2]==t[x1, t[x2, n[1]]]

Proof

We start by taking Critical Pair Lemma 24, and apply the substitution:

n[t[x1_, x2_]]->t[n[x1], x2]

which follows from Substitution Lemma 19.

Substitution Lemma 23

It can be shown that:

t[n[x1], x2]==t[x1, n[x2]]

Proof

We start by taking Substitution Lemma 22, and apply the substitution:

t[x1_, n[1]]->n[x1]

which follows from Substitution Lemma 21.

Substitution Lemma 24

It can be shown that:

t[a, n[n[a]]]==t[a, a]

Proof

We start by taking Hypothesis 1, and apply the substitution:

t[n[x1_], x2_]->t[x1, n[x2]]

which follows from Substitution Lemma 23.

Conclusion 1

We obtain the conclusion:

True

Proof

Take Substitution Lemma 24, and apply the substitution:

n[n[x1_]]->x1

which follows from Substitution Lemma 9.

6 + 7 + 7 + 6 + 3 = 29 steps
I really hope I didn't screw anything up, leave a comment if you think I did.
Lemma 1. a*0=0 (6 steps)

0 = a*0 + -(a*0)  axiom 3
= a*(0+0) + -(a*0) axiom 2
= (a*0 + a*0) + -(a*0) axiom 8
= a*0 + (a*0 + -(a*0)) axiom 1
= a*0 + 0 axiom 3
= a*0 axiom 2

Lemma 2. a*(-b) = -(a*b) (7 steps)

a*(-b) = a*(-b) + 0 axiom 2
= a*(-b) + (a*b + -(a*b)) axiom 3
= (a*(-b) + a*b) + -(a*b) axiom 1
= a*(-b+b) + -(a*b) axiom 8
= a*0 + -(a*b) axiom 3
= 0 + -(a*b) lemma 1
= -(a*b) axiom 2

Lemma 3. (-a)*b = -(a*b) (7 steps)
    same as above

Lemma 4. -(-(a)) = a (6 steps)

 -(-a) = (-(-a)) + 0    axiom 2
 = 0 + (-(-a))          axiom 4
 = (a + (-a)) + (-(-a)) axiom 3
 = a + ((-a) + (-(-a))) axiom 1
 = a + 0                axiom 3
 = a                    axiom 2

Theorem. -a*-a=0 (3 steps)

-a*-a = -(a*(-a)) lemma 3
= -(-(a*a)) lemma 2
= a*a lemma 4

Q.E.D.

I don't think you can make lemmas though

@HyperNeutrino I think that would just mean +6 steps for the reuse of lemma 1

@Stephen That would make more sense, yeah.

"Theorem. -a*-a=0" should be =a*a ?

@FunkyComputerMan What was your verdict on lemmas in the end?

@H.PWiz I don't have a problem with people using lemmas, but they cost as many steps as they are long each time they are used.  I would recommend against using them because they can get in the way of optimizations, but as far as I'm concerned this post is fine.

@FunkyComputerMan on, thanks.

going from "0 + -(a*b)" to "-(a*b)" in a single application of axiom 2 is not right. you need to use axiom 4 to swap the sides of the + first.

This solution actually takes (29 - 3) steps. You shouldn't include the 3 lines of your theorem because they are absorbed by the lemmas.

The way I read it is lemma 2/3 are 6 steps plus an instance of lemma 1 for 12 steps, lemma 4 is 6 steps, for a total of 30 steps. Am I missing something here?

In your lemma 2, you go from -b+b to 0 and appeal to Axiom 3. But Axiom 3 only says a + (-a) = 0, so you can't use that here without first proving that b = -(-b) (which you do only in Lemma 4).

Similarly in your lemma 2, you go from 0 + -(a*b) to -(a*b) and appeal to Axiom 2, which only says a + 0 = a. So it doesn't apply: you first need to commutativity (Axiom 4) before you can apply Axiom 2.

22 23 Steps
New answer, as my previous was flawed. Let me add some general comments first:

The problem does not allow to add terms on both sides of an equation; rather, we can only modify an initial string.
Multiplication is not assumed to be commutative.
We are given a unit 1, but it plays no role whatsoever in the puzzle because it is involved exclusively in the rules that define it.

Now for the proof (notice I define n = (-a) to simplify reading):
(-a)×(-a) :=
n×n =
n×n + 0 =                                [Ax. 2]
n×n + [n×a + -(n×a)] =                   [Ax. 3]
[n×n + n×a] + -(n×a) =                   [Ax. 1]
[n×(n+a)] + -(n×a) =                     [Ax. 8]
[n×(n+a) + 0] + -(n×a) =                 [Ax. 2]
[n×(n+a) + (n×a + -(n×a))] + -(n×a) =    [Ax. 3]
[(n×(n+a) + n×a) + -(n×a)] + -(n×a) =    [Ax. 1]
[n×((n+a) + a) + -(n×a)] + -(n×a) =      [Ax. 8]
[n×((a+n) + a) + -(n×a)] + -(n×a) =      [Ax. 4]
[n×(0 + a) + -(n×a)] + -(n×a) =          [Ax. 3]
[n×(a + 0) + -(n×a)] + -(n×a) =          [Ax. 4]
[n×a + -(n×a)] + -(n×a) =                [Ax. 2]
[(n+0)×a + -(n×a)] + -(n×a) =            [Ax. 2]
[(0+n)×a + -(n×a)] + -(n×a) =            [Ax. 4]
[((a+n)+n)×a + -(n×a)] + -(n×a) =        [Ax. 3]
[((a+n)×a+n×a) + -(n×a)] + -(n×a) =      [Ax. 9]
[(a+n)×a+(n×a + -(n×a))] + -(n×a) =      [Ax. 1]
[(a+n)×a + 0] + -(n×a) =                 [Ax. 3]
[(a+n)×a] + -(n×a) =                     [Ax. 2]
[a×a+n×a] + -(n×a) =                     [Ax. 9]
a×a+[n×a + -(n×a)] =                     [Ax. 1]
a×a+0 =                                  [Ax. 3]
a×a                                      [Ax. 2]

@H.PWiz why can't you go from n to 0 + n in one step? Isn't that just A2?  The rules do say The variables can also stand in for arbitrarily complex expressions

@jq170727 Axiom 2 only states that a + 0 = a not that 0 + a = a.  You need one extra commutative step to get from n to 0 + n.

@H.PWiz can't you read the axiom in reverse?

@jq170727 No you have to use commutativity for that.

34 steps
Lemma 1: 0=0*a (8 steps)
    0
A3: a*0 + -(a*0)
A4: -(a*0) + a*0
A2: -(a*0) + a*(0+0)
A8: -(a*0) + (a*0 + a*0)
A1: (-(a*0) + a*0) + a*0
A3: 0 + a*0
A4: a*0 + 0
A2: a*0

Theorem: -a*-a = a*a (49 steps)

    -a * -a
A2: (-a+0) * -a
A2: (-a+0) * (-a+0)
A3: (-a+(a+-a)) * (-a+0)
A3: (-a+(a+-a)) * (-a+(a+-a))
A8: -a*(-a+(a+-a)) + (a+-a)*(-a+(a+-a))
A8: -a*(-a+(a+-a)) + -a*(-a+(a+-a)) + a*(-a+(a+-a))
A3: -a*(-a+0)      + -a*(-a+(a+-a)) + a*(-a+(a+-a))
A3: -a*(-a+0)      + -a*(-a+0)      + a*(-a+(a+-a))
A8: -a*(-a+0)      + -a*(-a+0)      + a*-a + a*(a+-a)
A8: -a*(-a+0)      + -a*(-a+0)      + a*-a + a*a + a*-a
A2: -a*-a          + -a*(-a+0)      + a*-a + a*a + a*-a
A2: -a*-a          + -a*-a          + a*-a + a*a + a*-a
A8: -a*-a          + (-a+a)*-a             + a*a + a*-a
A3: -a*-a          + 0*-a                  + a*a + a*-a
L1: -a*-a          + 0                     + a*a + a*-a
A2: -a*-a                                  + a*a + a*-a
A4: a*a + -a*-a + a*-a
A8: a*a + (-a+a)*-a
A3: a*a + 0*-a
L1: a*a + 0
A2: a*a

I'm noticing a lack of parens after a while.  Because association costs steps, I think it would make it easier to verify your proof if you included the parens.

Am still improving and updating. Will try to include all the parens when I'm done.

25 steps
Note: based on the question, I'm assuming that the rules of logic (including equality) are implied and do not count towards the total step count. That is, things like "if x=y, then y=x" and "if ((P AND Q) AND R) then (P AND (Q AND R))" can be used implicitly.
Lemma Z [6 steps]: 0*a = 0:
0 = (0*a) + (-(0*a))       | Ax. 3
  = ((0+0)*a) + (-(0*a))   | Ax. 2
  = (0*a + 0*a) + (-(0*a)) | Ax. 9
  = 0*a + (0*a + (-(0*a))) | Ax. 1
  = 0*a + (0)              | Ax. 3
  = 0*a                    | Ax. 2

Lemma M [12 steps]: (-a)*b = -(a*b)
(-a)*b = (-a)*b + 0                | Ax. 2
       = (-a)*b + (a*b + (-(a*b))) | Ax. 3
       = ((-a)*b + a*b) + (-(a*b)) | Ax. 5
       = ((-a)+a)*b + (-(a*b))     | Ax. 9
       = 0*b + (-(a*b))            | Ax. 3
       = 0 + (-(a*b))              | Lem. Z [6]
       = -(a*b)                    | Ax. 2

Theorem [25 steps]: (-a)*(-a) = a*a
(-a)*(-a) = (-a)*(-a) + 0                | Ax. 2
          = 0 + (-a)*(-a)                | Ax. 4
          = (a*a + (-(a*a))) + (-a)*(-a) | Ax. 3
          = a*a + ((-(a*a)) + (-a)*(-a)) | Ax. 1
          = a*a + ((-a)*a + (-a)*(-a))   | Lem. M [12]
          = a*a + ((-a)*(a + (-a)))      | Ax. 8
          = a*a + ((-a)*0)               | Ax. 3
          = a*a + 0                      | Lem. Z [6]
          = a*a                          | Ax. 2

I feel like there's room for improvement here; for example, I use the commutative property of addition, though it feels like that should be unnecessary, since (-a)*(-a) = a*a is true in algebraic structures where addition is non-commutative. On the other hand, in those structures, the additive identity is commutative, and that's all I needed for the proof. I dunno. More generally, the proof's structure seems rather directionless; I just sort of threw stuff at the problem until it worked, so I bet there's some optimization to be done.
This was fun--thanks for the interesting and creative question OP! I haven't seen challenges like these before; hopefully proof-golf becomes a thing!

I see how the approach used in Lemma Z could make an equivalent proof for 0=(-a)*0 in 6 steps.  Technically it deserves its own Lemma though, doesn't it?

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


text:
BIU numbers (or Sumdivized numbers)
How to spot them
Take a positive integer k. Find its divisors. Find the distinct prime factors of each divisor. Sum all these factors together. If this number (sum) is a divisor of k (if the sum divides k) then, this number k, is a BIU number
Examples
Let's take the number 54
Find all the divisors: [1, 2, 3, 6, 9, 18, 27, 54]
Find the distinct prime factors of each divisor
NOTE: For the case of 1 we take as distinct prime factor 1
1  -> 1
2  -> 2
3  -> 3
6  -> 2,3
9  -> 3
18 -> 2,3
27 -> 3
54 -> 2,3

Now we take the sum of all these prime factors
1+2+3+2+3+3+2+3+3+2+3=27
27 divides 54 (leaves no remainder)
So, 54 is a BIU number.
Another (quick) example for k=55
Divisors: [1,5,11,55]
Sum of distinct prime factors: 1+5+11+5+11=33
33 is NOT a divisor of 55, that's why 55 is NOT a BIU number.
BIU numbers
Here are the first 20 of them:

1,21,54,290,735,1428,1485,1652,2262,2376,2580,2838,2862,3003,3875,4221,4745, 5525,6750,7050...

but this list goes on and there are many BIU numbers that are waiting to be descovered by you!
The Challenge
Given an integer n>0 as input, output the nth BIU number
Test Cases
Input->Output
1->1
2->21
42->23595
100->118300
200->415777
300->800175

This is codegolf.Shortest answer in bytes wins!

But 1 is not prime...

@Stephen thats why I said "For the case of 1 we take as distinct prime factor 1". This is my challenge and this is one of the rules of this challenge.I didn't say that 1 is prime.

Why are the numbers called "BIU"?

I'm not sure but I think that it has to do with bisexual intellectual unicorns using them in their everyday life (not in our universe of course...)

Downvoters, don't be shy. Share your thoughts with the rest of us.

Jelly, 16 15 bytes
ÆDÆfQ€SS‘ḍ
1Ç#Ṫ

Try it online!
Woohoo for builtins (but they mysteriously hide from me sometimes so -1 byte thanks to @HyperNeutrino)
How it Works
ÆDÆfQ€SS‘ḍ - define helper function: is input a BIU number?
ÆD             - divisors
  Æf           - list of prime factors
    Q€         - now distinct prime factors
      SS       - sum, then sum again ('' counts as 0)
        ‘      - add one (to account for '')
         ḍ     - does this divide the input?

1Ç#Ṫ - main link, input n
  #     - starting at
1          - 1
        - get the first n integers which meet:
 Ç         - helper link
   Ṫ    - tail

-1 byte using ÆfQ€ instead of ÆFḢ€€

but they mysteriously hide from me sometime "Jelly is a game of atom hide and programmer seek" ~ i cri everytim

I think you can save 1 byte with ÆDÆFSSḢ‘ḍ.

05AB1E, 9 bytes
µNNÑfOO>Ö

Uses teh 05AB1E encoding. Try it online!

Husk, 13 bytes
!fṠ¦ö→ΣṁoupḊN

Try it online!
Explantaion
  Ṡ¦ö→ΣṁoupḊ    Predicate: returns 1 if BIU, else 0.
           Ḋ    List of divisors
       ṁ        Map and then concatenate
        oup     unique prime factors
      Σ         Sum
    ö→          Add one
  Ṡ¦            Is the argument divisible by this result
 f          N   Filter the natural numbers by that predicate
!               Index

Mathematica, 85 bytes
If[#<2,1,n=#0[#-1];While[Count[(d=Divisors)@++n,1+Tr@Cases[d/@d@n,_?PrimeQ,2]]<1];n]&

Actually, 16 bytes
u⌠;÷♂y♂iΣu@%Y⌡╓N

Try it online!
Explanation:
u⌠;÷♂y♂iΣu@%Y⌡╓N
u⌠;÷♂y♂iΣu@%Y⌡╓   first n+1 numbers x starting with x=0 where
   ÷                divisors
    ♂y              prime factors of divisors
      ♂iΣu          sum of prime factors of divisors, plus 1
  ;       @%        x mod sum
            Y       is 0
               N  last number in list

Pyth, 22 bytes
e.f|qZ1!%Zhssm{Pd*M{yP

Try it here!
This is my first ever Pyth solution, I began learning it thanks to the recommendations of some very kind users in chat :-)... Took me about an hour to solve.
Explanation

e.f|qZ1!%Zhssm{Pd*M{yP  - Whole program. Q = input.

 .f                     - First Q integers with truthy results, using a variable Z.
     qZ1                - Is Z equal to 1?
   |                    - Logical OR.
                   {yP  - Prime factors, powerset, deduplicate.
                 *M     - Get the product of each. This chunck and ^ are for divisors.
              m}Pd      - Get the unique prime factors of each.
           ss           - Flatten and sum.
          h             - Increment (to handle that 1, bah)
       %Z               - Modulo the current integer by the sum above.
      !                 - Logical negation. 0 -> True, > 0 -> False.
e                       - Last element.

Haskell, 115 bytes
All of the list comprehensions here can probably be golfed down, but I'm not sure how. Golfing suggestions welcome! Try it online!
x!y=rem x y<1
b n=[a|a<-[1..],a!(1+sum[sum[z|z<-[2..m],m!z,and[not$z!x|x<-[2..z-1]]]|m<-[x|x<-[2..a],a!x]])]!!(n-1)

Ungolfing
This answer is actually three functions mashed together.
divisors a = [x | x <- [2..a], rem a x == 0]
sumPrimeDivs m = sum [z | z <- [2..m], rem m z == 0, and [rem z x /= 0 | x <- [2..z-1]]]
biu n = [a | a <- [1..], rem a (1 + sum [sumPrimeDivs m | m <- divisors a]) == 0] !! (n-1)

Japt, 22 21 17 bytes
I feel like the g function method should lead to a shorter solution, but I can't figure out how it works! Nope! Wrong method! But, in my defense, the i method didn't exist at the time.
1-indexed.
ÈvXâ mk câ x Ä}iU

Try it
ÈvXâ mk câ x Ä}iU     :Implicit input of integer U
È                     :Function taking an integer X as argument
 v                    :  Test X for divisibility by
  Xâ                  :    Divisors of X
     m                :    Map
      k               :      Prime factors
        c             :    Flatten after
         â            :      Deduplicating
           x          :    Reduce by addition
             Ä        :    Add 1
              }       :End function
               iU     :Get the Uth integer that returns true

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


text:
Polyglot the English Alphabet!
In this polyglot challenge, you will work together to figure out how to output all the 26 letters of the English alphabet!
How does this work?
For each answer, you must pick a new language (or a new major version of a language, for example, python 2 and python 3 are counted separately) that prints the next letter after the previous one.
Example of an answer.
Python 3 (Letter a):
print("a")

Other rules.

All letters are in lowercase.
Language must be Turing complete.
The same person cannot post twice in a row.
If an answer is found to be invalid it must be deleted.
Two users who post "at the same time" will have to let the earlier submission stand.
The same language must not be posted more than once.
Once we were done we keep going and start back at a.
It should print in all previous languages what it did in their original challenge

More things:

Set the sorting to oldest so this post works well.
Try not to make it impossible for the other person or else your post may be set as invalid.

Remember, GRUB shell is turning complete

what happens after z

You need to go off the previous answer... And I fixed that other problem @DJMcMayhem

It feels like you wanted to make this a polyglot

Yes @MistahFiggins sorry

I fixed the post I am sorry about the confusion

I suggest mentioning that it should print in all previous languages what it did in their original challenge. If that is what you meant, this is a duplicate of https://codegolf.stackexchange.com/questions/102370/add-a-language-to-a-polyglot.

@Scrooble Thanks... and it is not... that is numbers this is letters

@arodebaugh It's really just the same task; it doesn't add anything interesting to that challenge

@arodebaugh It is the same challenge, with slightly different output and a shorter lifespan. Aargh, you beat me to it, HyperNeutrino.

I hate this website! Why is everyone so picky. I am sorry if I am rude but I am a young programmer (16) and whenever I post anything on any of these sites I always get criticized for something and they never try to answer my question. Maybe I do this site wrong but it should be easy. This site and stack overflow

You might want to use the sandbox before you post a challenge next time. It helps you get feedback so that you don't have to edit the question a bunch when it gets to main. Sorry you feel that way :/

I think rule 8 clears it up the chaining confusion, but I would agree that it is a (near) duplicate of the other linked question.

@arodebaugh I would recommend you start with asking code-golf questions because they are usually the easiest to think of a unique idea for, specify, etc. answer-chaining is a bit harder to write and by all means avoid popularity-contests for your first while here because few have succeeded in that graveyard of closed questions :P Try using the sandbox, reading the help center, and asking in chat; we're happy to help new users get used to our system! As for SO... just read the help center :P

Any particular reason for the requirement of Turing completeness? That just excludes languages like Nhohnhehr that could otherwise take part in the challenge.

@Potato44 I mean some people argue that a programming language has to be turning complete "to be real" so I was just basing it off of that

Charcoal, 3 bytes
a⎚b

Try it online!
:P

You need to go off the previous answer

@arodebaugh What? What does that mean?

I fixed the post I am sorry about the confusion

Ok, does this fix it?

Yep it does if it outputs a  in Mathematica and b in charcoal.

I'm not really sure this works...?

Mathematica, 1 byte ...............
a

The thing I love about CodeGolf is that I am always amazed about how much people manage to golf their code. I mean one byte? That must be magic!