Rocq N’Roll is a software instrument and tool with type proof -> music. It parses Rocq proof tactics into Musical Instrument Digital Interface (MIDI) notes to generate musi- cal sound based on a proof state. ’Playing’ or ’performing’ a proof with Rocq N’Roll means stepping through it inter- actively to generate pitches that correspond to the step in the proof, with more complex chords and melodies coming from proof steps with multiple suboperations (i.e. automated tactics). Rocq N’ Roll is primarily an artistic tool, but it may also have interesting use cases in helping Rocq users con- ceptualize proof deautomation.