Even without AI, software can come to the aid of the mathematician. I will give
an example of how having both symbolic computation (with Magma) and first order logic
(in Walnut) at one's fingertips, conjectures in combinatorics can be discovered and proved.
The example was inspired by a course given, with Robbert Fokkink, for Dutch Master students.
The example concerns generalizations of OEIS entry A026471, an infinite sequence starting
1, 2, 3, 4, 5, 13, 14, 15, 25, 26, 27, 37, 38, 48, 49, 50, 60, 61, ...
where, after the initial 3 values, the next one is the least positive integer exceeding the
previous ones that is not the sum of 3 previous entries in the sequence.
Eventually we proved that `almost all' sequences `of this kind' behave `very predictably';
all three of these vague terms will be made very precise in the talk --- and open questions also
still remain!