Let HT denotes the statement of Hindman’s theorem. Within RCA0 one can prove that:
1. HT implies ACA0
2. HT can be proved in ACA0+.
An open question is the strength of Hindman’s theorem.
Is HT equivalent to ACA0+ , or to ACA0, or does it lie strictly between them?