How can one prove that a shunting-yard algorithm always returns a correct expression in RPN? I cannot find any proof in the internet.
The shunting-yard algorithm was introduced in Dijkstra's article Making a Translator for ALGOL-60 (APIC Bulletin no7, 1961; see this PDF, from p.22; also published in Annual Review in Automatic Programming, 7:3–11, 1963 and available from Science Direct if your institution has a subscription). Pages 7–9 of the article (pp.28–30 of the PDF) explain how the algorithm works and argue its correctness. It's not a formal proof but it looks like it contains everything you should need to produce one.