Brilliant and so encouraging! >because of limitations in reasoning skills and training data One would assume that mathematical literature and training data wo

Brilliant and so encouraging! >because of limitations in reasoning skills and training data One would assume that mathematical literature and training data would be abundant. Is there a simple example that could help appreciate the Gemini bridge layer mentioned in the blog which produces the input for RL in Lean?