چرا مفهوم معادلت در ریاضی انقدر پیچیده است؟
در ریاضیات، اهمیت تساوی و مفهوم برابری مجموعه‌ها بسیار مهم است. با پیشرفت نظریه مجموعه‌ها، تعریف دقیقی برای تساوی دو مجموعه ارائه شد که بر اساس آن، مجموعه‌های با عناصر متفاوت می‌توانند برابر باشند. این معنی تساوی در ریاضیات تخصصی استفاده می‌شود و با تساوی در زبان معمولی ممکن است متفاوت باشد.
یک‌ریختی متعارف این امکان را فراهم می‌کند که دو مجموعه با عناصر مختلف را تساوی کنیم. اما در برنامه‌های کامپیوتری، این مفهوم می‌تواند به مسائلی منجر شود که نیاز به دقت و وضوح بیشتری دارند. برای حل این مسئله، نظریه‌ی نوع هموتوپی به عنوان یک راه‌حل پیشنهاد شده است که در آن تعاریف تساوی متفاوت در ریاضیات سنتی و برنامه‌های کامپیوتری، یکسان شده و از آن استفاده می‌شود.
مشکلات موجود در ارتباط بین ریاضیات و برنامه‌های کامپیوتری نشانگر ضرورت بررسی دقیق‌تر و بازنگری نظریه‌های ریاضیاتی است که از آن‌ها برای اثبات و حل مسائل استفاده می‌شود. به نظر می‌رسد که برای حل این مشکل، نیاز به تطبیق و به‌روزرسانی نظریه‌ها و اصول ریاضی داریم تا بتوانیم به بهبود سیستم‌های کامپیوتری برسیم.
با پیشرفت نظریه‌ی مجموعه‌ها، ریاضیدانها به این نتیجه رسیدند که دو مجموعه در صورتی برابر هستند که روشی واضح برای ایجاد نگاشت بین آن‌ها وجود داشته باشد، حتی اگر دقیقا دارای عنصرهای یکسان نباشند. برای درک چرایی این موضوع، مجموعه‌های {1,2,3} و {a,b,c} را درنظر بگیرید.
واضح است که عنصرهای هر مجموعه متفاوت هستند، بنابراین مجموعه‌ها برابر نیستند؛ اما همیشه روش‌هایی برای نگاشت بین دو مجموعه وجود دارد؛ به‌طوری‌که هر حرف الفبا به یک عدد تصویر می‌شود. ریاضیدانها به این نوع نگاشت یک‌ریختی یا ایزومورفیسم می‌گویند.
در این نمونه، یک‌ریختی‌های متعددی وجود دارند، زیرا می‌توانید انتخاب کنید که هر عدد به یک حرف الفبا تخصیص پیدا کند، اما در بسیاری از نمونه‌ها تنها یک انتخاب واضح وجود دارد که در این صورت به آن یک‌ریختی متعارف می‌گویند.
از آنجا که یک‌ریختی متعارف دو مجموعه تنها راه ممکن برای اتصال آن‌ها است، بسیاری از ریاضیدانها این اتصال را نوعی تساوی درنظر می‌گیرند، گرچه از نظر تخصصی به معنی مفهوم تساوی که اغلب افراد می‌شناسند، نیست. کوین بوزارد از کالج سلطنتی لندن می‌گوید:
این مجموعه‌ها به شیوه‌ای کاملا طبیعی با یکدیگر منطبق هستند و ریاضیدانها آن‌ها را مساوی نیز درنظر می‌گیرند
برای ریاضیدانها داشتن دو تعریف از تساوی هنگام نوشتن مقاله یا ارائه نگران‌کننده نیست، زیرا معنا همیشه از زمینه قابل فهم است، اما مشکلاتی را برای برنامه‌های کامپیوتری به دنبال دارد که به دستورالعمل‌های دقیق نیاز دارند.
برای حل این مشکل، پژوهشگرها به بررسی چگونگی کاربرد یک‌ریختی متعارف به‌عنوان تساوی و مشکلات آن در سیستم‌های اثبات کامپیوتری پرداختند. به‌ویژه پژوهش الکساندر گروتندیک، یکی از ریاضیدانان پیشتاز قرن بیستم امروزه به‌سختی می‌تواند فرمول‌بندی شود؛ زیرا هیچ‌کدام از سیستم‌ها به روشی که ریاضی‌دان‌هایی مثل گروتندیک از تساوی استفاده می‌کردند، نمی‌توانند این مسئله را درک کنند.
مشکل فوق ریشه در روش‌های اثبات ریاضیدانها نیز دارد. برای اثبات هر چیزی در ابتدا باید فرضیه‌هایی موسوم به اصل یا آکسیوم را بسازید که بدون نیاز به اثبات صحیح هستند و چارچوبی منطقی را فراهم می‌کنند. از ابتدای قرن بیستم، ریاضیدانها به مجموعه‌ای از آکسیوم‌ها در نظریه‌ی مجموعه‌ها تکیه کردند که شالوده‌ای محکم را فراهم می‌کنند.
برنامه‌های کامپیوتری در درک نسبی تساوی به مشکل می‌خورند
در واقع دیگر نیازی نبود در محاسبات روزمره‌شان به طور مستقیم از آکسیوم‌ها استفاده کنند؛ چرا که معمولا فرض می‌شود این اصل‌ها به صورت پیش‌فرض درست عمل کنند. به بیان دیگر، شما برای پختن یک غذا نیازی به دانستن عملکرد داخلی وسایل آشپزخانه ندارید.
در نتیجه به‌عنوان یک ریاضی‌دان تا حدی می‌دانید که چه کار می‌کنید و نیازی نیست نگران آن باشید. بااین‌حال زمانی که پای کامپیوترها به میان بیاید، مسئله تا حدی متفاوت می‌شود؛ زیرا کامپیوترها درست به شیوه‌ای محاسبات ریاضی را انجام می‌دهند که گویی قرار است برای هر وعده‌ی غذایی وسایل آشپزخانه را از ابتدا بسازند؛ بنابراین وقتی قرار است اثبات مسئله‌ای را بر عهده‌ی کامپیوتر بگذارید، باید همه چیز را به صورت دقیق و واضح برای آن تعریف کنید.
به باور برخی ریاضیدانها برای حل این مشکل باید مبانی ریاضیات را بازتعریف کنیم تا یک‌ریختی‌های متعارف و تساوی یکسان شوند. سپس می‌توانیم برنامه‌های کامپیوتری را حول محور این تعریف‌ها بسازیم.
به این منظور تلاش‌هایی در حوزه‌ی یک رشته‌ی ریاضی موسوم به نظریه‌ی نوع هموتوپی در جریان هستند. بر اساس این نظریه، تساوی سنتی و یک‌ریختی متعارف به‌صورت یکسان تعریف می‌شوند. به‌جای اینکه دستیارهای اثبات موجود را تغییر دهیم تا با یک‌ریختی متعارف سازگار باشند، باید نظریه‌ی نوع را تطبیق دهیم و از دستیارهای اثبات جایگزین برای کار مستقیم با آن استفاده کنیم.
بوزارد طرفدار این راه‌حل نیست چرا که زمان زیادی را صرف استفاده از ابزارهای فعلی برای فرمول‌بندی اثبات‌های ریاضی کرده است. به عقیده‌ی بوزارد، آکسیوم‌های ریاضی باید همان‌طور که هستند باقی بمانند و در عوض باید سیستم‌های موجود را تغییر داد. او می‌گوید:
شاید راه‌حل این مشکل این باشد که صرفا ریاضیدانها را به حال خود بگذاریم. به سختی می‌توان ریاضیدانها را تغییر داد پس بهتر است در عوض برای بهبود سیستم‌های کامپیوتری تلاش کنیم.
