Finding the least positive integer satisfying a quantified statement

For the first question: you can use ForAll (as you used $\forall$!) also in Mathematica. Once you have acquired a region, you can minimize argument constrained on it:

ArgMin[{n, 
  Resolve[ForAll[m, m >= n && Element[n, Integers], 
    m^2 0.2 (1 - 0.2^2)^m < 1 && m > 0]]}, n]

227

If you take a hard look at the statement above, you may notice it's not exactly the same as the original question: it requires all real values of m larger or equal to integer n to satisfy the inequality, not just all integer values of m... well, it seems Resolve handles this well, but can't make the same reasoning when m is constrained to integers.

I don't know an answer to the second question.