Wikipedia and a few websites (and a few mathoverflow answers) say there is a constructive proof of the Brouwer fixed point theorem, some others say no. The argument for a constructive proof is always the same. The Brouwer fixed point theorem is equivalent to some other results (Miranda, Sperner) where some algorithm produces some object (trichromatic triangle etc) related to a potential fixed point, but in fact, one also need an additional compactness argument to conclude, and this last step does not appear to me to be constructive.

I am not a logician, so my question is

can one give a mathematical rigorous meaning to the following statement: "there is no constructive proof to the Brouwer fixed point theorem"?

Wikipedia and a few websites (and a few mathoverflow answers) say there is a constructive proof of the Brouwer fixed point theorem, some others say no. The argument for a constructive proof is always the same. The Brouwer fixed point theorem is equivalent to some other results (Miranda, Sperner) where some algorithm produces some object (trichromatic triangle etc) related to a potential fixed point, but in fact, one also needs an additional compactness argument to conclude, and this last step does not appear to me to be constructive.

I am not a logician, so my question is

can one give a mathematical rigorous meaning to the following statement: "there is no constructive proof to the Brouwer fixed point theorem"?