W dniu środa, 1 stycznia 2020 23:25:50 UTC+1 użytkownik Maciej Sobczak napisał:
> > > W temacie eksploracji zagadnień matematycznych Wolfram nie ma merytorycznej
konkurencji.
> >
> > Polimeryzowałbym.
>
> Super, noworoczne otwarcie. :-)
>
> > 1. Jest droga.
>
> Przecież pisałem o merytorycznej konkurencji.
>
> I oczywiście zależy co to znaczy "droga". Są programy, przy zakupie których
Mathematica ginie w finansowym szumie.
>
> > 2. Nie potrafi tego co MISAR. Ok, MISAR to zupełnie inna półka.
> > Choć niewątpliwie matematyka.
>
> https://en.wikipedia.org/wiki/Misar
>
> Poproszę o dalsze wskazówki. To jest tak inna półka, że nawet tej półki nie
znalazłem.

Na ile mogę się domyślić, chodzi o projekt MIZAR, zapoczątkowany przez Andrzeja
Trybulca z Białegostoku.

http://mizar.org/

Projekt podobny np. do Coq albo systemu LCF Robina Milnera (dla którego powstał język
ML).

W niektórych kręgach notacja Mizara jest popularną notacją do formalizacji dowodów
matematycznych