### Alex Nelson

Shared publicly -I am sad to learn that

I knew

Sadly, Trybulec opted to have the Mizar system be closed source, fearing people might make slight alterations which would ultimately cause an irreparable "drift" from the "pure" Mizar system. Consequently, it is difficult to verify the verifier. (Amusingly, researchers discovered serious problems with the Mizar system's verified statements a few years ago, and now there's a desparate movement to double check the Mizar library of user submitted proofs in another system, like HOL or Isabelle...which seems like it still won't resolve the underlying issue of verifying the Mizar verifer

At any rate, he was a brilliant man, and reading his mailing list contributions, he came off as someone very caring, light hearted, and humorous.

https://en.wikipedia.org/wiki/Andrzej_Trybulec

**Andrzej Trybulec**passed away September 11, 2013.I knew

*of*him from his work on the Mizar system...seeing as he*invented*that particular automated theorem prover. It was revolutionary in design, modelling the input source code after how mathematicians really write proofs (compared to the other popular approach, of writing down useful directions and hints the computer might use at trying to prove a given theorem).Sadly, Trybulec opted to have the Mizar system be closed source, fearing people might make slight alterations which would ultimately cause an irreparable "drift" from the "pure" Mizar system. Consequently, it is difficult to verify the verifier. (Amusingly, researchers discovered serious problems with the Mizar system's verified statements a few years ago, and now there's a desparate movement to double check the Mizar library of user submitted proofs in another system, like HOL or Isabelle...which seems like it still won't resolve the underlying issue of verifying the Mizar verifer

*works properly*.)At any rate, he was a brilliant man, and reading his mailing list contributions, he came off as someone very caring, light hearted, and humorous.

https://en.wikipedia.org/wiki/Andrzej_Trybulec

1

3 comments

Ah, many thanks!

Add a comment...