Post #1717617

@meena the proof assistant Mizar used to work like that, you had to submit a proof to the math library to get access to the source code.