در دنیای ریاضیات، بعضی مفاهیم آن‌قدر عادی به نظر می‌رسند که هرگز درباره‌شان شک نمی‌کنیم؛ اما حالا ریاضیدانان بر سر یکی از پایه‌ای‌ترین نشانه‌های این علم یعنی علامت مساوی (=)اختلاف‌نظر دارند!
این موضوع نه‌تنها باعث جنجال در جامعه علمی شده، بلکه چالشی بزرگ برای برنامه‌های کامپیوتری ایجاد کرده که به پردازش اثبات‌های ریاضی می‌پردازند.
علامت مساوی نخستین بار در سال ۱۵۵۷ میلادی توسط رابرت رکورد، ریاضیدان ولزی، معرفی شد. اما مفهوم «برابری» در ریاضیات از همان ابتدا پیچیدگی‌هایی داشت که در طول قرن‌ها تغییر کرده است. امروزه، برخی از ریاضیدانان معتقدند که مفهوم مساوی باید شامل شباهت‌های ساختاری (ایزومورفیسم) هم باشد، نه فقط برابری عددی!
مشکل اصلی زمانی به اوج رسید که برنامه‌نویسان سعی کردند از رایانه‌ها برای اثبات قضایای ریاضی استفاده کنند. کوین بازارد، ریاضیدان بریتانیایی، متوجه شد که سیستم‌های کامپیوتری نمی‌توانند به درستی مفهوم مساوی را پردازش کنند، چون این مفهوم برای ریاضیدانان به‌شکل غیررسمی و با تفسیرهای مختلف استفاده می‌شود.
آیا باید تعریف «مساوی» را در ریاضیات تغییر داد؟ یا بهتر است ماشین‌ها را طوری طراحی کنیم که روش‌های پیچیده‌تری برای درک این مفهوم داشته باشند؟ این چالش اساسی، هنوز پاسخی قطعی ندارد.
