- Copilot. A cloud artificial intelligence assistant for programming. Developped by OpenAI using a version of ChatGPT, it was initially trained on the corpus of code available on GitHub. I have recently tested it for Python and Julia as a plugin for Visual Studio Code. It allows notably interaction via comments and code completions. My feeling is that it may help programmers trained to use it, but it remains for the moment a gadget, particularly efficient if you code something standard or connected to an open source standard. However the potentialities are amazing, and it will probably change the face of coding.
- Lean. A proof assistant, in other words a computer language and environment that allows to check mathematical proofs. More pragmatic than Coq, it has a vivid and boiling users community and has the potential to produce a revolution for mathematicians. It does not seem to be connected with Copilot or something similar, a matter of time? Lean is a Microsoft Research open source project hosted on GitHub. We are still waiting for the connection between Mathematica type software with Copilot or Lean type software. We are still waiting for the fusion between mathematics and computer science practices.
Copilot, Lean, and GitHub are related to Microsoft, who is now a major actor in the crucial domains of cloud computing, open source, and artificial intelligence. It is interesting to see how former major innovative actors such as Google, Amazon, Facebook, and Apple were beaten, and how the artificial intelligence revolution is still coming from the USA, without notable contribution from the European or Asian capitalisms. For now, Europe and Asia mostly contribute with brains. This American renewed success largerly depends on an American Higher Education capitalism.