UMa alpha, Dubhe UMa beta, Merak UMa gamma, Phecda UMa delta, Megrez UMa epsilon, Alioth UMa eta, Alkaid UMa zeta, Mizar
Mizar the star
Mizar project

Welcome to Megrez services

by Grzegorz Bancerek

Megrez services are partially supported by Japan Society for the Promotion of Science
Mizar (the zeta star in Ursa Major constellation - see above) is a language designed by Andrzej Trybulec to approximate mathematical vernacular in formal style for computer proof verification. The Mizar project, besides the language, concerns software tools (see also Mizar sources and kernel programs), a library (see index of Mizar articles), and a hyperlinked journal. The development in the Mizar project is coordinated by the Association of Mizar Users. Mizar system can be downloaded from this site or others. Everyone may contribute an Mizar article to the Mizar library (see also page How to submit an article to the MML).
Services
What's new?
Mirror of Mizar Main Site
MML Query
FM proof-read
Mizar statistics
Mizar remote processing
Download
Registration
Mizar Forum
     
Mizar User Service
     mus@mizar.uwb.edu.pl
Mizar TWiki
Tools
Mizar system
Mizar mode for emacs
Bibart

Ursa Major (Great Bear) Constellation
Megrez is the least light star in the Big Dipper asterism.
It joins the tail containing the Mizar star
with the main part of the Big Dipper (and the Great Bear).
background (© Copyright by T. Credner, AlltheSky.com)
Resources
Mizar classes
MML Guide
Continuous Lattices
Jordan Curve Theorem
Circuits
Merak presentation system
Mizarians
Grzegorz Bancerek (e-mail: bancerek@mizar.org)