Post #2798892

I participated into a study on how I use Lean They anonymized the transcript for some research repository, and asked me to approve that. I pasted that transscript into Gemini, and immediately got: SPEAKER_01 is an advanced user and developer of the Lean theorem prover. While the transcript doesn't explicitly state a name, the speaker provides very specific biographical and technical details that strongly suggest they are Joachim Breitner. Key Identifying Details: […] Anonymization is hard.