ბლოგი

Lean-ის თეორემების დამმტკიცებელი სანდოობის კითხვების წინაშე დგას, რადგან AI-ის ავტოფორმალიზაცია ვითარდება

Lean-ი, მათემატიკოსებში ყველაზე გავრცელებული თეორემების დამმტკიცებელი, სანდოობის კითხვების წინაშე დგას 2026 წლის ზაფხულის ხარვეზების შემდეგ, მაშინ როცა AI-ის ავტოფორმალიზაციამ 2025 და 2026 წლებში მსხვილი პროექტები დაასრულა.