Voltage divider with ADC
A reading of 1023 means your ADC is off scale, that is, its input voltage is higher than the reference.

Be aware that you can select several different sources for the ADC reference, including VCC (which from your question context I suspect you thought you were using), but it can also be 1.1v, and an external voltage. Off the top of my head, I don't know which is the default.

Once you have selected VCC as your ADC reference, then your formula for the voltages based on R1 and R2 is correct.