В последние десятилетия в мире появились интеллектуальные обучаю-щие системы, в том числе основанные на автоматическом доказательстве тео-рем, а также доступные он-лайн. Некоторые из них были коммерциализированы. Одним из лидеров является компания CarnegieLearning, продающая ИОС для изучения математики сотням школ в США. В России такие разработки ведутся пока еще в сравнительно небольших масштабах и зачастую не доходят до практического применения. В данной работе рассматриваются интеллектуальные обучающие системы с автоматическим доказательством теорем, их архитектуры, функциональные возможности и методы их реализации.